rlvect_1.miz



    begin

    definition

      struct ( addLoopStr) RLSStruct (# the carrier -> set,

the ZeroF -> Element of the carrier,

the addF -> BinOp of the carrier,

the Mult -> Function of [: REAL , the carrier:], the carrier #)

       attr strict strict;

    end

    registration

      cluster non empty for RLSStruct;

      existence

      proof

        set ZS = the non empty set, O = the Element of ZS, F = the BinOp of ZS, G = the Function of [: REAL , ZS:], ZS;

        take RLSStruct (# ZS, O, F, G #);

        thus the carrier of RLSStruct (# ZS, O, F, G #) is non empty;

      end;

    end

    reserve V for non empty RLSStruct;

    reserve x,y,y1 for set;

    definition

      let V be RLSStruct;

      mode VECTOR of V is Element of V;

    end

    theorem :: RLVECT_1:1

    for V be non empty 1-sorted, v be Element of V holds v in V;

    reserve v for VECTOR of V;

    reserve a,b for Real;

    definition

      let V, v;

      let a be Real;

      :: RLVECT_1:def1

      func a * v -> Element of V equals (the Mult of V . (a,v));

      coherence

      proof

        reconsider a as Element of REAL by XREAL_0:def 1;

        (the Mult of V . (a,v)) is Element of V;

        hence thesis;

      end;

    end

    theorem :: RLVECT_1:2

    for V be non empty addMagma, v,w be Element of V holds (v + w) = (the addF of V . (v,w));

    registration

      let ZS be non empty set, O be Element of ZS, F be BinOp of ZS, G be Function of [: REAL , ZS:], ZS;

      cluster RLSStruct (# ZS, O, F, G #) -> non empty;

      coherence ;

    end

    definition

      let IT be addMagma;

      :: RLVECT_1:def2

      attr IT is Abelian means

      : Def2: for v,w be Element of IT holds (v + w) = (w + v);

      :: RLVECT_1:def3

      attr IT is add-associative means

      : Def3: for u,v,w be Element of IT holds ((u + v) + w) = (u + (v + w));

    end

    definition

      let IT be addLoopStr;

      :: RLVECT_1:def4

      attr IT is right_zeroed means

      : Def4: for v be Element of IT holds (v + ( 0. IT)) = v;

    end

    definition

      let IT be non empty RLSStruct;

      :: RLVECT_1:def5

      attr IT is vector-distributive means

      : Def5: for a holds for v,w be VECTOR of IT holds (a * (v + w)) = ((a * v) + (a * w));

      :: RLVECT_1:def6

      attr IT is scalar-distributive means

      : Def6: for a, b holds for v be VECTOR of IT holds ((a + b) * v) = ((a * v) + (b * v));

      :: RLVECT_1:def7

      attr IT is scalar-associative means

      : Def7: for a, b holds for v be VECTOR of IT holds ((a * b) * v) = (a * (b * v));

      :: RLVECT_1:def8

      attr IT is scalar-unital means

      : Def8: for v be VECTOR of IT holds (1 * v) = v;

    end

    definition

      :: RLVECT_1:def9

      func Trivial-RLSStruct -> strict RLSStruct equals RLSStruct (# { 0 }, op0 , op2 , ( pr2 ( REAL , { 0 })) #);

      coherence ;

    end

    registration

      cluster Trivial-RLSStruct -> 1 -element;

      coherence ;

    end

    registration

      cluster strict Abelian add-associative non empty for addMagma;

      existence

      proof

        take S = Trivial-addMagma ;

        thus S is strict;

        thus S is Abelian by STRUCT_0:def 10;

        thus S is add-associative by STRUCT_0:def 10;

        thus thesis;

      end;

    end

    registration

      cluster strict Abelian add-associative right_zeroed right_complementable non empty for addLoopStr;

      existence

      proof

        take S = Trivial-addLoopStr ;

        thus S is strict;

        thus S is Abelian by STRUCT_0:def 10;

        thus S is add-associative by STRUCT_0:def 10;

        thus S is right_zeroed by STRUCT_0:def 10;

        thus thesis;

      end;

    end

    registration

      cluster strict Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital for non empty RLSStruct;

      existence

      proof

        take S = Trivial-RLSStruct ;

        thus S is strict;

        thus S is Abelian by STRUCT_0:def 10;

        thus S is add-associative by STRUCT_0:def 10;

        thus S is right_zeroed by STRUCT_0:def 10;

        thus S is right_complementable

        proof

          let x be Element of S;

          take x;

          thus thesis by STRUCT_0:def 10;

        end;

        thus for a, b holds for v be VECTOR of S holds ((a + b) * v) = ((a * v) + (b * v)) by STRUCT_0:def 10;

        thus for a holds for v,w be VECTOR of S holds (a * (v + w)) = ((a * v) + (a * w)) by STRUCT_0:def 10;

        thus for a, b holds for v be VECTOR of S holds ((a * b) * v) = (a * (b * v)) by STRUCT_0:def 10;

        thus for v be VECTOR of S holds (1 * v) = v by STRUCT_0:def 10;

      end;

    end

    definition

      mode RealLinearSpace is Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty RLSStruct;

    end

    definition

      let V be Abelian addMagma, v,w be Element of V;

      :: original: +

      redefine

      func v + w;

      commutativity by Def2;

    end

    

     Lm1: for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V st (v + w) = ( 0. V) holds (w + v) = ( 0. V)

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V;

      assume

       A1: (v + w) = ( 0. V);

      consider u be Element of V such that

       A2: (w + u) = ( 0. V) by ALGSTR_0:def 11;

      (w + v) = (w + (v + (w + u))) by A2, Def4

      .= (w + ((v + w) + u)) by Def3

      .= ((w + (v + w)) + u) by Def3

      .= (w + u) by A1, Def4;

      hence thesis by A2;

    end;

    theorem :: RLVECT_1:3

    

     Th3: for V be add-associative right_zeroed right_complementable addLoopStr holds V is right_add-cancelable

    proof

      let V be add-associative right_zeroed right_complementable addLoopStr;

      let v be Element of V;

      consider v1 be Element of V such that

       A1: (v + v1) = ( 0. V) by ALGSTR_0:def 11;

      let u,w be Element of V;

      assume

       A2: (u + v) = (w + v);

      

      thus u = (u + ( 0. V)) by Def4

      .= ((u + v) + v1) by A1, Def3

      .= (w + ( 0. V)) by A1, A2, Def3

      .= w by Def4;

    end;

    theorem :: RLVECT_1:4

    

     Th4: for V be add-associative right_zeroed right_complementable non empty addLoopStr, v be Element of V holds (v + ( 0. V)) = v & (( 0. V) + v) = v

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr, v be Element of V;

      consider w be Element of V such that

       A1: (v + w) = ( 0. V) by ALGSTR_0:def 11;

      thus

       A2: (v + ( 0. V)) = v by Def4;

      (w + v) = ( 0. V) by A1, Lm1;

      hence thesis by A2, A1, Def3;

    end;

    registration

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let v1 be zero Element of V;

      let v2 be Element of V;

      reduce (v1 + v2) to v2;

      reducibility

      proof

        v1 = ( 0. V) by STRUCT_0:def 12;

        hence thesis by Th4;

      end;

      reduce (v2 + v1) to v2;

      reducibility

      proof

        v1 = ( 0. V) by STRUCT_0:def 12;

        hence thesis by Th4;

      end;

    end

    definition

      let V be non empty addLoopStr;

      let v be Element of V;

      assume

       A1: V is add-associative right_zeroed right_complementable;

      :: original: -

      redefine

      :: RLVECT_1:def10

      func - v means

      : Def10: (v + it ) = ( 0. V);

      compatibility

      proof

        let IT be Element of V;

        consider v1 be Element of V such that

         A2: (v + v1) = ( 0. V) by A1, ALGSTR_0:def 11;

        

         A3: V is right_add-cancelable by A1, Th3;

        

         A4: v is left_complementable

        proof

          take v1;

          ((v1 + v) + v1) = (v1 + ( 0. V)) by A1, A2

          .= (( 0. V) + v1) by A1;

          hence thesis by A3, ALGSTR_0:def 4;

        end;

        ((v + ( - v)) + v) = (v + (( - v) + v)) by A1

        .= (v + ( 0. V)) by A3, A4, ALGSTR_0:def 13

        .= (( 0. V) + v) by A1;

        hence IT = ( - v) implies (v + IT) = ( 0. V) by A3, ALGSTR_0:def 4;

        assume

         A5: (v + IT) = ( 0. V);

        

        thus IT = (( 0. V) + IT) by A1

        .= ((( - v) + v) + IT) by A3, A4, ALGSTR_0:def 13

        .= (( - v) + ( 0. V)) by A1, A5

        .= ( - v) by A1;

      end;

    end

    

     Lm2: for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,u be Element of V holds ex w be Element of V st (v + w) = u

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let v,u be Element of V;

      take w = (( - v) + u);

      

      thus (v + w) = ((v + ( - v)) + u) by Def3

      .= (( 0. V) + u) by Def10

      .= u;

    end;

    definition

      let V be addLoopStr;

      let v,w be Element of V;

      :: original: -

      redefine

      :: RLVECT_1:def11

      func v - w equals (v + ( - w));

      correctness ;

    end

    theorem :: RLVECT_1:5

    

     Th5: for V be add-associative right_zeroed right_complementable non empty addLoopStr, v be Element of V holds (v + ( - v)) = ( 0. V) & (( - v) + v) = ( 0. V)

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr, v be Element of V;

      thus (v + ( - v)) = ( 0. V) by Def10;

      hence thesis by Lm1;

    end;

    theorem :: RLVECT_1:6

    

     Th6: for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V holds (v + w) = ( 0. V) implies v = ( - w)

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let v,w be Element of V;

      assume (v + w) = ( 0. V);

      then (w + v) = ( 0. V) by Lm1;

      hence thesis by Def10;

    end;

    theorem :: RLVECT_1:7

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,u be Element of V holds ex w be Element of V st (v + w) = u by Lm2;

    theorem :: RLVECT_1:8

    

     Th8: for V be add-associative right_zeroed right_complementable non empty addLoopStr, w,u,v1,v2 be Element of V st (w + v1) = (w + v2) or (v1 + w) = (v2 + w) holds v1 = v2

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let w,u,v1,v2 be Element of V;

       A1:

      now

        assume

         A2: (v1 + w) = (v2 + w);

        

        thus v1 = (v1 + ( 0. V))

        .= (v1 + (w + ( - w))) by Th5

        .= ((v1 + w) + ( - w)) by Def3

        .= (v2 + (w + ( - w))) by A2, Def3

        .= (v2 + ( 0. V)) by Th5

        .= v2;

      end;

      now

        assume

         A3: (w + v1) = (w + v2);

        

        thus v1 = (( 0. V) + v1)

        .= ((( - w) + w) + v1) by Th5

        .= (( - w) + (w + v1)) by Def3

        .= ((( - w) + w) + v2) by A3, Def3

        .= (( 0. V) + v2) by Th5

        .= v2;

      end;

      hence thesis by A1;

    end;

    theorem :: RLVECT_1:9

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V holds (v + w) = v or (w + v) = v implies w = ( 0. V)

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V;

      assume (v + w) = v or (w + v) = v;

      then (v + w) = (v + ( 0. V)) or (w + v) = (( 0. V) + v);

      hence thesis by Th8;

    end;

    theorem :: RLVECT_1:10

    

     Th10: for V be add-associative right_zeroed right_complementable scalar-distributive scalar-unital vector-distributive non empty RLSStruct, v be Element of V holds a = 0 or v = ( 0. V) implies (a * v) = ( 0. V)

    proof

      let V be add-associative right_zeroed right_complementable scalar-distributive scalar-unital vector-distributive non empty RLSStruct, v be Element of V;

      assume a = 0 or v = ( 0. V);

      per cases ;

        suppose

         A1: a = 0 ;

        (v + ( 0 * v)) = ((1 * v) + ( 0 * v)) by Def8

        .= ((1 + 0 ) * v) by Def6

        .= (v + ( 0. V)) by Def8;

        hence thesis by A1, Th8;

      end;

        suppose

         A2: v = ( 0. V);

        ((a * ( 0. V)) + (a * ( 0. V))) = (a * (( 0. V) + ( 0. V))) by Def5

        .= ((a * ( 0. V)) + ( 0. V));

        hence thesis by A2, Th8;

      end;

    end;

    registration

      let V be add-associative right_zeroed right_complementable scalar-distributive scalar-unital vector-distributive non empty RLSStruct;

      let v be zero Element of V;

      let r be Real;

      reduce (r * v) to v;

      reducibility

      proof

        v = ( 0. V) by STRUCT_0:def 12;

        hence thesis by Th10;

      end;

    end

    theorem :: RLVECT_1:11

    

     Th11: for V be add-associative right_zeroed right_complementable scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V holds (a * v) = ( 0. V) implies a = 0 or v = ( 0. V)

    proof

      let V be add-associative right_zeroed right_complementable scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V;

      assume that

       A1: (a * v) = ( 0. V) and

       A2: a <> 0 ;

      

      thus v = (1 * v) by Def8

      .= (((a " ) * a) * v) by A2, XCMPLX_0:def 7

      .= ((a " ) * ( 0. V)) by A1, Def7

      .= ( 0. V);

    end;

    theorem :: RLVECT_1:12

    

     Th12: for V be add-associative right_zeroed right_complementable non empty addLoopStr holds ( - ( 0. V)) = ( 0. V)

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      

      thus ( 0. V) = (( 0. V) + ( - ( 0. V))) by Def10

      .= ( - ( 0. V));

    end;

    registration

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let v be zero Element of V;

      reduce ( - v) to v;

      reducibility

      proof

        v = ( 0. V) by STRUCT_0:def 12;

        hence thesis by Th12;

      end;

    end

    registration

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let v1 be Element of V;

      let v2 be zero Element of V;

      reduce (v1 - v2) to v1;

      reducibility ;

    end

    theorem :: RLVECT_1:13

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, v be Element of V holds (v - ( 0. V)) = v;

    theorem :: RLVECT_1:14

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, v be Element of V holds (( 0. V) - v) = ( - v);

    theorem :: RLVECT_1:15

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, v be Element of V holds (v - v) = ( 0. V) by Def10;

    theorem :: RLVECT_1:16

    

     Th16: for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-unital vector-distributive non empty RLSStruct, v be Element of V holds ( - v) = (( - 1) * v)

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-unital vector-distributive non empty RLSStruct, v be Element of V;

      (v + (( - 1) * v)) = ((1 * v) + (( - 1) * v)) by Def8

      .= ((1 + ( - 1)) * v) by Def6

      .= ( 0. V) by Th10;

      

      hence ( - v) = (( - v) + (v + (( - 1) * v)))

      .= ((( - v) + v) + (( - 1) * v)) by Def3

      .= (( 0. V) + (( - 1) * v)) by Def10

      .= (( - 1) * v);

    end;

    registration

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let v be Element of V;

      reduce ( - ( - v)) to v;

      reducibility

      proof

        (v + ( - v)) = ( 0. V) by Def10;

        hence thesis by Th6;

      end;

    end

    theorem :: RLVECT_1:17

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, v be Element of V holds ( - ( - v)) = v;

    theorem :: RLVECT_1:18

    

     Th18: for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V holds ( - v) = ( - w) implies v = w

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let v,w be Element of V;

      assume ( - v) = ( - w);

      

      hence v = ( - ( - w))

      .= w;

    end;

    theorem :: RLVECT_1:19

    

     Th19: for V be add-associative right_zeroed right_complementable scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V holds v = ( - v) implies v = ( 0. V)

    proof

      let V be add-associative right_zeroed right_complementable scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V;

      assume v = ( - v);

      

      then ( 0. V) = (v + v) by Def10

      .= ((1 * v) + v) by Def8

      .= ((1 * v) + (1 * v)) by Def8

      .= ((1 + 1) * v) by Def6

      .= (2 * v);

      hence thesis by Th11;

    end;

    theorem :: RLVECT_1:20

    for V be add-associative right_zeroed right_complementable scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V holds (v + v) = ( 0. V) implies v = ( 0. V)

    proof

      let V be add-associative right_zeroed right_complementable scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V;

      assume (v + v) = ( 0. V);

      then v = ( - v) by Def10;

      hence thesis by Th19;

    end;

    theorem :: RLVECT_1:21

    

     Th21: for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V holds (v - w) = ( 0. V) implies v = w

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let v,w be Element of V;

      assume (v - w) = ( 0. V);

      then ( - v) = ( - w) by Def10;

      hence thesis by Th18;

    end;

    theorem :: RLVECT_1:22

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, u,v be Element of V holds ex w be Element of V st (v - w) = u

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let u,v be Element of V;

      consider w be Element of V such that

       A1: (v + w) = u by Lm2;

      take ( - w);

      thus thesis by A1;

    end;

    theorem :: RLVECT_1:23

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, w,v1,v2 be Element of V st (w - v1) = (w - v2) holds v1 = v2

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let w,v1,v2 be Element of V;

      assume (w - v1) = (w - v2);

      then ( - v1) = ( - v2) by Th8;

      hence thesis by Th18;

    end;

    theorem :: RLVECT_1:24

    

     Th24: for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V holds (a * ( - v)) = (( - a) * v)

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V;

      

      thus (a * ( - v)) = (a * (( - 1) * v)) by Th16

      .= ((a * ( - 1)) * v) by Def7

      .= (( - a) * v);

    end;

    theorem :: RLVECT_1:25

    

     Th25: for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V holds (a * ( - v)) = ( - (a * v))

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V;

      

      thus (a * ( - v)) = (( - (1 * a)) * v) by Th24

      .= ((( - 1) * a) * v)

      .= (( - 1) * (a * v)) by Def7

      .= ( - (a * v)) by Th16;

    end;

    theorem :: RLVECT_1:26

    for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V holds (( - a) * ( - v)) = (a * v)

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V;

      

      thus (( - a) * ( - v)) = (( - ( - a)) * v) by Th24

      .= (a * v);

    end;

    

     Lm3: for V be add-associative right_zeroed right_complementable non empty addLoopStr, u,w be Element of V holds ( - (u + w)) = (( - w) + ( - u))

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr, u,w be Element of V;

      ((u + w) + (( - w) + ( - u))) = (u + (w + (( - w) + ( - u)))) by Def3

      .= (u + ((w + ( - w)) + ( - u))) by Def3

      .= (u + (( 0. V) + ( - u))) by Def10

      .= ( 0. V) by Def10;

      hence thesis by Def10;

    end;

    theorem :: RLVECT_1:27

    

     Th27: for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V holds (v - (u + w)) = ((v - w) - u)

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let v,u,w be Element of V;

      

      thus (v - (u + w)) = (v + (( - w) + ( - u))) by Lm3

      .= ((v - w) - u) by Def3;

    end;

    theorem :: RLVECT_1:28

    for V be add-associative non empty addLoopStr, v,u,w be Element of V holds ((v + u) - w) = (v + (u - w)) by Def3;

    theorem :: RLVECT_1:29

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V holds (v - (u - w)) = ((v - u) + w)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr;

      let v,u,w be Element of V;

      

      thus (v - (u - w)) = (v - (u + ( - w)))

      .= ((v - u) - ( - w)) by Th27

      .= ((v - u) + w);

    end;

    theorem :: RLVECT_1:30

    

     Th30: for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V holds ( - (v + w)) = (( - w) - v)

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let v,w be Element of V;

      

      thus ( - (v + w)) = (( 0. V) - (v + w))

      .= ((( 0. V) - w) - v) by Th27

      .= (( - w) - v);

    end;

    theorem :: RLVECT_1:31

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V holds ( - (v + w)) = (( - w) + ( - v)) by Lm3;

    theorem :: RLVECT_1:32

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V holds (( - v) - w) = (( - w) - v)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr;

      let v,w be Element of V;

      

      thus (( - v) - w) = ( - (w + v)) by Th30

      .= (( - w) - v) by Th30;

    end;

    theorem :: RLVECT_1:33

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V holds ( - (v - w)) = (w + ( - v))

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let v,w be Element of V;

      

      thus ( - (v - w)) = (( - ( - w)) + ( - v)) by Lm3

      .= (w + ( - v));

    end;

    theorem :: RLVECT_1:34

    

     Th34: for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v,w be Element of V holds (a * (v - w)) = ((a * v) - (a * w))

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v,w be Element of V;

      

      thus (a * (v - w)) = ((a * v) + (a * ( - w))) by Def5

      .= ((a * v) - (a * w)) by Th25;

    end;

    theorem :: RLVECT_1:35

    

     Th35: for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V holds ((a - b) * v) = ((a * v) - (b * v))

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V;

      

      thus ((a - b) * v) = ((a + ( - b)) * v)

      .= ((a * v) + (( - b) * v)) by Def6

      .= ((a * v) + (b * ( - v))) by Th24

      .= ((a * v) - (b * v)) by Th25;

    end;

    theorem :: RLVECT_1:36

    for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v,w be Element of V holds a <> 0 & (a * v) = (a * w) implies v = w

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v,w be Element of V;

      assume that

       A1: a <> 0 and

       A2: (a * v) = (a * w);

      ( 0. V) = ((a * v) - (a * w)) by A2, Def10

      .= (a * (v - w)) by Th34;

      then (v - w) = ( 0. V) by A1, Th11;

      hence thesis by Th21;

    end;

    theorem :: RLVECT_1:37

    for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V holds v <> ( 0. V) & (a * v) = (b * v) implies a = b

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V;

      assume that

       A1: v <> ( 0. V) and

       A2: (a * v) = (b * v);

      ( 0. V) = ((a * v) - (b * v)) by A2, Def10

      .= ((a - b) * v) by Th35;

      then (( - b) + a) = 0 by A1, Th11;

      hence thesis;

    end;

    reserve V for non empty addLoopStr;

    reserve F for FinSequence-like PartFunc of NAT , V;

    reserve f,f9,g for sequence of V;

    reserve v,u for Element of V;

    reserve j,k,n for Nat;

    definition

      let V;

      let F be the carrier of V -valued FinSequence;

      :: RLVECT_1:def12

      func Sum (F) -> Element of V means

      : Def12: ex f st it = (f . ( len F)) & (f . 0 ) = ( 0. V) & for j be Nat, v st j < ( len F) & v = (F . (j + 1)) holds (f . (j + 1)) = ((f . j) + v);

      existence

      proof

        defpred P[ set] means for F be the carrier of V -valued FinSequence st ( len F) = $1 holds ex u st ex f st u = (f . ( len F)) & (f . 0 ) = ( 0. V) & for j, v st j < ( len F) & v = (F . (j + 1)) holds (f . (j + 1)) = ((f . j) + v);

        

         A1: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n;

          assume

           A2: for F be the carrier of V -valued FinSequence st ( len F) = n holds ex u st ex f st u = (f . ( len F)) & (f . 0 ) = ( 0. V) & for j, v st j < ( len F) & v = (F . (j + 1)) holds (f . (j + 1)) = ((f . j) + v);

          let F be the carrier of V -valued FinSequence;

          

           A3: ( rng F) c= the carrier of V by RELAT_1:def 19;

          then

          reconsider F1 = F as FinSequence of V by FINSEQ_1:def 4;

          reconsider G = (F1 | ( Seg n)) as FinSequence of V by FINSEQ_1: 18;

          assume

           A4: ( len F) = (n + 1);

          then ( dom F) = ( Seg (n + 1)) by FINSEQ_1:def 3;

          then (n + 1) in ( dom F) by FINSEQ_1: 4;

          then (F . (n + 1)) in ( rng F) by FUNCT_1:def 3;

          then

          reconsider u1 = (F . (n + 1)) as Element of V by A3;

          

           A5: n < (n + 1) by NAT_1: 13;

          then

          consider u, f such that u = (f . ( len G)) and

           A6: (f . 0 ) = ( 0. V) and

           A7: for j, v st j < ( len G) & v = (G . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by A2, A4, FINSEQ_1: 17;

          defpred P[ set, set] means for j st $1 = j holds (j < (n + 1) implies $2 = (f . $1)) & ((n + 1) <= j implies for u st u = (F . (n + 1)) holds $2 = ((f . ( len G)) + u));

          

           A8: for k be Element of NAT qua non empty set holds ex v be Element of V st P[k, v]

          proof

            let k be Element of NAT qua non empty set;

            reconsider i = k as Element of NAT ;

             A9:

            now

              assume

               A10: (n + 1) <= i;

              take v = ((f . ( len G)) + u1);

              let j;

              assume k = j;

              hence j < (n + 1) implies v = (f . k) by A10;

              assume (n + 1) <= j;

              let u2 be Element of V;

              assume u2 = (F . (n + 1));

              hence v = ((f . ( len G)) + u2);

            end;

            now

              assume

               A11: i < (n + 1);

              take v = (f . k);

              let j such that

               A12: k = j;

              thus j < (n + 1) implies v = (f . k);

              thus (n + 1) <= j implies for u st u = (F . (n + 1)) holds v = ((f . ( len G)) + u) by A11, A12;

            end;

            hence thesis by A9;

          end;

          consider f9 be sequence of the carrier of V such that

           A13: for k be Element of NAT holds P[k, (f9 . k)] from FUNCT_2:sch 3( A8);

          

           A14: for k be Nat holds P[k, (f9 . k)]

          proof

            let k be Nat;

            k in NAT by ORDINAL1:def 12;

            hence thesis by A13;

          end;

          take z = (f9 . (n + 1));

          take f99 = f9;

          thus z = (f99 . ( len F)) by A4;

          thus (f99 . 0 ) = ( 0. V) by A6, A14;

          let j, v;

          assume that

           A15: j < ( len F) and

           A16: v = (F . (j + 1));

          

           A17: ( len G) = n by A4, A5, FINSEQ_1: 17;

           A18:

          now

            assume

             A19: j = n;

            then (f99 . (j + 1)) = ((f . j) + v) by A17, A14, A16;

            hence (f99 . (j + 1)) = ((f99 . j) + v) by A5, A14, A19;

          end;

           A20:

          now

            assume

             A21: j < n;

            then

             A22: (j + 1) < (n + 1) by XREAL_1: 6;

            1 <= (1 + j) & (j + 1) <= n by A21, NAT_1: 11, NAT_1: 13;

            then (j + 1) in ( Seg n) by FINSEQ_1: 1;

            then

             A23: v = (G . (j + 1)) by A16, FUNCT_1: 49;

            j < ( len G) by A4, A5, A21, FINSEQ_1: 17;

            then

             A24: (f . (j + 1)) = ((f . j) + v) by A7, A23;

            j < (n + 1) by A21, NAT_1: 13;

            then (f . (j + 1)) = ((f9 . j) + v) by A14, A24;

            hence (f99 . (j + 1)) = ((f99 . j) + v) by A14, A22;

          end;

          j <= n by A4, A15, NAT_1: 13;

          hence (f99 . (j + 1)) = ((f99 . j) + v) by A20, A18, XXREAL_0: 1;

        end;

        

         A25: P[ 0 ]

        proof

          reconsider f = ( NAT --> ( 0. V)) as sequence of the carrier of V;

          let F be the carrier of V -valued FinSequence;

          assume

           A26: ( len F) = 0 ;

          take u = (f . ( len F));

          take f9 = f;

          thus u = (f9 . ( len F)) & (f9 . 0 ) = ( 0. V) by FUNCOP_1: 7;

          let j;

          thus for v st j < ( len F) & v = (F . (j + 1)) holds (f9 . (j + 1)) = ((f9 . j) + v) by A26;

        end;

        for n holds P[n] from NAT_1:sch 2( A25, A1);

        hence thesis;

      end;

      uniqueness

      proof

        let v1,v2 be Element of V;

        given f such that

         A27: v1 = (f . ( len F)) and

         A28: (f . 0 ) = ( 0. V) and

         A29: for j, v st j < ( len F) & v = (F . (j + 1)) holds (f . (j + 1)) = ((f . j) + v);

        given f9 such that

         A30: v2 = (f9 . ( len F)) and

         A31: (f9 . 0 ) = ( 0. V) and

         A32: for j, v st j < ( len F) & v = (F . (j + 1)) holds (f9 . (j + 1)) = ((f9 . j) + v);

        defpred P[ Nat] means $1 <= ( len F) implies (f . $1) = (f9 . $1);

        now

          

           A33: ( rng F) c= the carrier of V by RELAT_1:def 19;

          let k;

          assume

           A34: k <= ( len F) implies (f . k) = (f9 . k);

          assume

           A35: (k + 1) <= ( len F);

          1 <= (k + 1) & ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3, NAT_1: 11;

          then (k + 1) in ( dom F) by A35, FINSEQ_1: 1;

          then (F . (k + 1)) in ( rng F) by FUNCT_1:def 3;

          then

          reconsider u1 = (F . (k + 1)) as Element of V by A33;

          

           A36: k < ( len F) by A35, NAT_1: 13;

          then (f . (k + 1)) = ((f . k) + u1) by A29;

          hence (f . (k + 1)) = (f9 . (k + 1)) by A32, A34, A36;

        end;

        then

         A37: for k st P[k] holds P[(k + 1)];

        

         A38: P[ 0 ] by A28, A31;

        for k holds P[k] from NAT_1:sch 2( A38, A37);

        hence thesis by A27, A30;

      end;

    end

    

     Lm4: ( Sum ( <*> the carrier of V)) = ( 0. V)

    proof

      set S = ( <*> the carrier of V);

      ex f st ( Sum S) = (f . ( len S)) & (f . 0 ) = ( 0. V) & for j, v st j < ( len S) & v = (S . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by Def12;

      hence thesis;

    end;

    

     Lm5: ( len F) = 0 implies ( Sum F) = ( 0. V)

    proof

      assume ( len F) = 0 ;

      then F = ( <*> the carrier of V);

      hence thesis by Lm4;

    end;

    theorem :: RLVECT_1:38

    

     Th38: for F,G be FinSequence of V holds ( len F) = (( len G) + 1) & G = (F | ( dom G)) & v = (F . ( len F)) implies ( Sum F) = (( Sum G) + v)

    proof

      let F,G be FinSequence of V;

      assume that

       A1: ( len F) = (( len G) + 1) and

       A2: G = (F | ( dom G)) and

       A3: v = (F . ( len F));

      consider g such that

       A4: ( Sum G) = (g . ( len G)) and

       A5: (g . 0 ) = ( 0. V) and

       A6: for j, v st j < ( len G) & v = (G . (j + 1)) holds (g . (j + 1)) = ((g . j) + v) by Def12;

      consider f such that

       A7: ( Sum F) = (f . ( len F)) and

       A8: (f . 0 ) = ( 0. V) and

       A9: for j, v st j < ( len F) & v = (F . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by Def12;

      defpred P[ Nat] means for H be FinSequence of V holds ( len H) = $1 & H = (F | ( Seg $1)) & ( len H) <= ( len G) implies (f . ( len H)) = (g . ( len H));

      now

        let k;

        assume

         A10: for H be FinSequence of V st ( len H) = k & H = (F | ( Seg k)) & ( len H) <= ( len G) holds (f . ( len H)) = (g . ( len H));

        let H be FinSequence of V;

        assume that

         A11: ( len H) = (k + 1) and

         A12: H = (F | ( Seg (k + 1))) and

         A13: ( len H) <= ( len G);

        1 <= (k + 1) & (k + 1) <= ( len F) by A1, A11, A13, NAT_1: 12;

        then (k + 1) in ( dom F) by FINSEQ_3: 25;

        then

        reconsider v = (F . (k + 1)) as Element of V by FUNCT_1: 102;

        1 <= (k + 1) by NAT_1: 12;

        then (k + 1) in ( Seg ( len G)) by A11, A13, FINSEQ_1: 1;

        then (k + 1) in ( dom G) by FINSEQ_1:def 3;

        then

         A14: v = (G . (k + 1)) by A2, FUNCT_1: 47;

        reconsider H1 = H as FinSequence of V;

        reconsider p = (H1 | ( Seg k)) as FinSequence of V by FINSEQ_1: 18;

        

         A15: k <= ( len H) by A11, NAT_1: 12;

        then ( Seg k) c= ( Seg (k + 1)) by A11, FINSEQ_1: 5;

        then

         A16: p = (F | ( Seg k)) by A12, FUNCT_1: 51;

        k < (k + 1) by XREAL_1: 29;

        then k < ( len G) by A11, A13, XXREAL_0: 2;

        then

         A17: (g . (k + 1)) = ((g . k) + v) by A6, A14;

        

         A18: ( len G) < ( len F) by A1, XREAL_1: 29;

        k <= ( len G) by A13, A15, XXREAL_0: 2;

        then k < ( len F) by A18, XXREAL_0: 2;

        then

         A19: (f . (k + 1)) = ((f . k) + v) by A9;

        ( len p) = k by A15, FINSEQ_1: 17;

        hence (f . ( len H)) = (g . ( len H)) by A10, A11, A13, A15, A16, A19, A17, XXREAL_0: 2;

      end;

      then

       A20: for k st P[k] holds P[(k + 1)];

      

       A21: ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3;

      

       A22: P[ 0 ] by A8, A5;

      for k holds P[k] from NAT_1:sch 2( A22, A20);

      then (f . ( len G)) = (g . ( len G)) by A2, A21;

      hence thesis by A1, A3, A7, A9, A4, XREAL_1: 29;

    end;

    reserve V for RealLinearSpace;

    reserve v for VECTOR of V;

    reserve F,G,H,I for FinSequence of V;

    theorem :: RLVECT_1:39

    ( len F) = ( len G) & (for k, v st k in ( dom F) & v = (G . k) holds (F . k) = (a * v)) implies ( Sum F) = (a * ( Sum G))

    proof

      defpred P[ set] means for H, I st ( len H) = ( len I) & ( len H) = $1 & (for k, v st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = (a * v)) holds ( Sum H) = (a * ( Sum I));

      

       A1: ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3;

      now

        let n;

        assume

         A2: for H, I st ( len H) = ( len I) & ( len H) = n & for k, v st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = (a * v) holds ( Sum H) = (a * ( Sum I));

        let H, I;

        assume that

         A3: ( len H) = ( len I) and

         A4: ( len H) = (n + 1) and

         A5: for k, v st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = (a * v);

        reconsider p = (H | ( Seg n)), q = (I | ( Seg n)) as FinSequence of the carrier of V by FINSEQ_1: 18;

        

         A6: n <= (n + 1) by NAT_1: 12;

        then

         A7: ( len q) = n by A3, A4, FINSEQ_1: 17;

        

         A8: ( len p) = n by A4, A6, FINSEQ_1: 17;

         A9:

        now

          ( len p) <= ( len H) by A4, A6, FINSEQ_1: 17;

          then

           A10: ( Seg ( len p)) c= ( Seg ( len H)) by FINSEQ_1: 5;

          

           A11: ( dom p) = ( Seg n) by A4, A6, FINSEQ_1: 17;

          let k, v;

          assume that

           A12: k in ( Seg ( len p)) and

           A13: v = (q . k);

          ( dom q) = ( Seg n) by A3, A4, A6, FINSEQ_1: 17;

          then (I . k) = (q . k) by A8, A12, FUNCT_1: 47;

          then (H . k) = (a * v) by A5, A12, A13, A10;

          hence (p . k) = (a * v) by A8, A12, A11, FUNCT_1: 47;

        end;

        1 <= (n + 1) by NAT_1: 11;

        then (n + 1) in ( dom H) & (n + 1) in ( dom I) by A3, A4, FINSEQ_3: 25;

        then

        reconsider v1 = (H . (n + 1)), v2 = (I . (n + 1)) as VECTOR of V by FUNCT_1: 102;

        

         A14: v1 = (a * v2) by A4, A5, FINSEQ_1: 4;

        

         A15: ( dom q) = ( Seg ( len q)) by FINSEQ_1:def 3;

        ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

        

        hence ( Sum H) = (( Sum p) + v1) by A4, A8, Th38

        .= ((a * ( Sum q)) + (a * v2)) by A2, A8, A7, A9, A14

        .= (a * (( Sum q) + v2)) by Def5

        .= (a * ( Sum I)) by A3, A4, A7, A15, Th38;

      end;

      then

       A16: for n st P[n] holds P[(n + 1)];

      now

        let H, I;

        assume that

         A17: ( len H) = ( len I) and

         A18: ( len H) = 0 and for k, v st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = (a * v);

        ( Sum H) = ( 0. V) by A18, Lm5;

        hence ( Sum H) = (a * ( Sum I)) by A17, A18, Lm5, Th10;

      end;

      then

       A19: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A19, A16);

      hence thesis by A1;

    end;

    theorem :: RLVECT_1:40

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, F,G be FinSequence of V st ( len F) = ( len G) & (for k holds for v be Element of V st k in ( dom F) & v = (G . k) holds (F . k) = ( - v)) holds ( Sum F) = ( - ( Sum G))

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, F,G be FinSequence of V;

      defpred P[ set] means for H,I be FinSequence of V st ( len H) = ( len I) & ( len H) = $1 & (for k holds for v be Element of V st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = ( - v)) holds ( Sum H) = ( - ( Sum I));

      

       A1: ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3;

      now

        let n;

        assume

         A2: for H,I be FinSequence of V st ( len H) = ( len I) & ( len H) = n & for k holds for v be Element of V st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = ( - v) holds ( Sum H) = ( - ( Sum I));

        let H,I be FinSequence of V;

        assume that

         A3: ( len H) = ( len I) and

         A4: ( len H) = (n + 1) and

         A5: for k holds for v be Element of V st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = ( - v);

        reconsider p = (H | ( Seg n)), q = (I | ( Seg n)) as FinSequence of the carrier of V by FINSEQ_1: 18;

        

         A6: n <= (n + 1) by NAT_1: 12;

        then

         A7: ( len q) = n by A3, A4, FINSEQ_1: 17;

        

         A8: ( len p) = n by A4, A6, FINSEQ_1: 17;

         A9:

        now

          ( len p) <= ( len H) by A4, A6, FINSEQ_1: 17;

          then

           A10: ( Seg ( len p)) c= ( Seg ( len H)) by FINSEQ_1: 5;

          

           A11: ( dom p) = ( Seg n) by A4, A6, FINSEQ_1: 17;

          let k;

          let v be Element of V;

          assume that

           A12: k in ( Seg ( len p)) and

           A13: v = (q . k);

          ( dom q) = ( Seg n) by A3, A4, A6, FINSEQ_1: 17;

          then (I . k) = (q . k) by A8, A12, FUNCT_1: 47;

          then (H . k) = ( - v) by A5, A12, A13, A10;

          hence (p . k) = ( - v) by A8, A12, A11, FUNCT_1: 47;

        end;

        1 <= (n + 1) by NAT_1: 11;

        then (n + 1) in ( dom H) & (n + 1) in ( dom I) by A3, A4, FINSEQ_3: 25;

        then

        reconsider v1 = (H . (n + 1)), v2 = (I . (n + 1)) as Element of V by FUNCT_1: 102;

        

         A14: v1 = ( - v2) by A4, A5, FINSEQ_1: 4;

        

         A15: ( dom q) = ( Seg ( len q)) by FINSEQ_1:def 3;

        ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

        

        hence ( Sum H) = (( Sum p) + v1) by A4, A8, Th38

        .= (( - ( Sum q)) + ( - v2)) by A2, A8, A7, A9, A14

        .= ( - (( Sum q) + v2)) by Lm3

        .= ( - ( Sum I)) by A3, A4, A7, A15, Th38;

      end;

      then

       A16: for n st P[n] holds P[(n + 1)];

      now

        let H,I be FinSequence of V;

        assume that

         A17: ( len H) = ( len I) & ( len H) = 0 and for k holds for v be Element of V st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = ( - v);

        ( Sum H) = ( 0. V) & ( Sum I) = ( 0. V) by A17, Lm5;

        hence ( Sum H) = ( - ( Sum I));

      end;

      then

       A18: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A18, A16);

      hence thesis by A1;

    end;

    theorem :: RLVECT_1:41

    

     Th41: for V be add-associative right_zeroed non empty addLoopStr, F,G be FinSequence of V holds ( Sum (F ^ G)) = (( Sum F) + ( Sum G))

    proof

      let V be add-associative right_zeroed non empty addLoopStr, F,G be FinSequence of V;

      defpred P[ set] means for G be FinSequence of V st ( len G) = $1 holds ( Sum (F ^ G)) = (( Sum F) + ( Sum G));

      

       A1: for k st P[k] holds P[(k + 1)]

      proof

        let k;

        assume

         A2: for G be FinSequence of V st ( len G) = k holds ( Sum (F ^ G)) = (( Sum F) + ( Sum G));

        let H be FinSequence of V;

        reconsider p = (H | ( Seg k)) as FinSequence of V by FINSEQ_1: 18;

        

         A3: ( rng H) c= the carrier of V by FINSEQ_1:def 4;

        assume

         A4: ( len H) = (k + 1);

        then

         A5: ( dom H) = ( Seg (k + 1)) by FINSEQ_1:def 3;

        then

         A6: (k + 1) in ( dom H) by FINSEQ_1: 4;

        then (H . (k + 1)) in ( rng H) by FUNCT_1:def 3;

        then

        reconsider v = (H . (k + 1)) as Element of V by A3;

        

         A7: k <= (k + 1) by NAT_1: 12;

         A8:

        now

          let n be Nat;

          assume n in ( dom p);

          then n in ( Seg k) by A4, A7, FINSEQ_1: 17;

          hence (p . n) = (H . n) by FUNCT_1: 49;

        end;

        

         A9: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

        

         A10: ( Seg ( len (F ^ p))) = ( Seg (( len F) + ( len p))) by FINSEQ_1: 22;

        

         A11: ( dom (F ^ H)) = ( Seg ( len (F ^ H))) by FINSEQ_1:def 3

        .= ( Seg (( len F) + ( len H))) by FINSEQ_1: 22;

        

         A12: ( dom (F ^ p)) = ( Seg ( len (F ^ p))) by FINSEQ_1:def 3;

        ( dom p) = ( Seg k) by A4, A7, FINSEQ_1: 17;

        then

         A13: ( dom p) c= ( dom H) by A5, A7, FINSEQ_1: 5;

         A14:

        now

          let x be object;

          assume

           A15: x in ( dom (F ^ p));

          then

          reconsider n = x as Element of NAT ;

           A16:

          now

            assume not n in ( dom F);

            then

             A17: not n in ( Seg ( len F)) by FINSEQ_1:def 3;

            

             A18: 1 <= n by A12, A15, FINSEQ_1: 1;

            then ( len F) <= n by A17, FINSEQ_1: 1;

            then

            consider j be Nat such that

             A19: n = (( len F) + j) by NAT_1: 10;

             A20:

            now

              assume not j <= k;

              then

               A21: (( len F) + k) < n by A19, XREAL_1: 6;

              n <= (( len F) + ( len p)) by A12, A10, A15, FINSEQ_1: 1;

              hence contradiction by A4, A7, A21, FINSEQ_1: 17;

            end;

            now

              assume not 1 <= j;

              then j = 0 by NAT_1: 14;

              hence contradiction by A17, A18, A19, FINSEQ_1: 1;

            end;

            then j in ( Seg k) by A20, FINSEQ_1: 1;

            then

             A22: j in ( dom p) by A4, A7, FINSEQ_1: 17;

            then ((F ^ p) . n) = (p . j) & ((F ^ H) . n) = (H . j) by A13, A19, FINSEQ_1:def 7;

            hence ((F ^ p) . x) = ((F ^ H) . x) by A8, A22;

          end;

          now

            assume

             A23: n in ( dom F);

            then ((F ^ p) . n) = (F . n) by FINSEQ_1:def 7;

            hence ((F ^ p) . x) = ((F ^ H) . x) by A23, FINSEQ_1:def 7;

          end;

          hence ((F ^ p) . x) = ((F ^ H) . x) by A16;

        end;

        

         A24: ( len p) = k by A4, A7, FINSEQ_1: 17;

        then (( len F) + ( len p)) <= (( len F) + ( len H)) by A4, A7, XREAL_1: 7;

        then ( Seg ( len (F ^ p))) c= ( dom (F ^ H)) by A11, A10, FINSEQ_1: 5;

        then ( dom (F ^ p)) = (( dom (F ^ H)) /\ ( Seg ( len (F ^ p)))) by A12, XBOOLE_1: 28;

        

        then

         A25: (F ^ p) = ((F ^ H) | ( Seg ( len (F ^ p)))) by A14, FUNCT_1: 46

        .= ((F ^ H) | ( dom (F ^ p))) by FINSEQ_1:def 3;

         A26:

        now

          let n be Nat;

          assume n in ( dom <*v*>);

          then n in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

          then n = 1 by TARSKI:def 1;

          hence (H . (( len p) + n)) = ( <*v*> . n) by A24, FINSEQ_1:def 8;

        end;

        ( dom H) = ( Seg (( len p) + ( len <*v*>))) by A5, A24, FINSEQ_1: 39;

        then H = (p ^ <*v*>) by A8, A26, FINSEQ_1:def 7;

        then (F ^ H) = ((F ^ p) ^ <*v*>) by FINSEQ_1: 32;

        then ( len (F ^ H)) = (( len (F ^ p)) + ( len <*v*>)) by FINSEQ_1: 22;

        then

         A27: ( len (F ^ H)) = (( len (F ^ p)) + 1) by FINSEQ_1: 39;

        v = ((F ^ H) . (( len F) + ( len H))) by A4, A6, FINSEQ_1:def 7

        .= ((F ^ H) . ( len (F ^ H))) by FINSEQ_1: 22;

        

        hence ( Sum (F ^ H)) = (( Sum (F ^ p)) + v) by A27, A25, Th38

        .= ((( Sum F) + ( Sum p)) + v) by A2, A24

        .= (( Sum F) + (( Sum p) + v)) by Def3

        .= (( Sum F) + ( Sum H)) by A4, A24, A9, Th38;

      end;

      

       A28: P[ 0 ]

      proof

        let G be FinSequence of V;

        assume ( len G) = 0 ;

        then G = ( <*> the carrier of V);

        then (F ^ G) = F & ( Sum G) = ( 0. V) by Lm4, FINSEQ_1: 34;

        hence thesis by Def4;

      end;

      for k holds P[k] from NAT_1:sch 2( A28, A1);

      then ( len G) = ( len G) implies thesis;

      hence thesis;

    end;

    reserve V for add-associative right_zeroed right_complementable non empty addLoopStr;

    reserve F for FinSequence of V;

    reserve v,v1,v2,u,w for Element of V;

    reserve j,k for Nat;

    

     Lm6: for V be add-associative right_zeroed right_complementable non empty addLoopStr, v be Element of V holds ( Sum <*v*>) = v

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr, v be Element of V;

      set S = <*v*>;

      consider f be sequence of the carrier of V such that

       A1: ( Sum S) = (f . ( len S)) and

       A2: (f . 0 ) = ( 0. V) & for j holds for v be Element of V st j < ( len S) & v = (S . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by Def12;

       0 < 1;

      then

      consider j such that

       A3: j < ( len S);

      

       A4: ( len S) = 1 by FINSEQ_1: 39;

      

      then

       A5: (S . (j + 1)) = (S . ( 0 + 1)) by A3, NAT_1: 14

      .= v by FINSEQ_1: 40;

      j = 0 by A4, A3, NAT_1: 14;

      

      then (f . 1) = (( 0. V) + v) by A2, A5

      .= v;

      hence thesis by A1, FINSEQ_1: 39;

    end;

    theorem :: RLVECT_1:42

    for V be Abelian add-associative right_zeroed non empty addLoopStr, F,G be FinSequence of V st ( rng F) = ( rng G) & F is one-to-one & G is one-to-one holds ( Sum F) = ( Sum G)

    proof

      let V be Abelian add-associative right_zeroed non empty addLoopStr, F,G be FinSequence of V;

      defpred P[ set] means for H,I be FinSequence of V st ( len H) = $1 & ( rng H) = ( rng I) & H is one-to-one & I is one-to-one holds ( Sum H) = ( Sum I);

      

       A1: ( len F) = ( len F);

      now

        let k;

        assume

         A2: for H,I be FinSequence of V st ( len H) = k & ( rng H) = ( rng I) & H is one-to-one & I is one-to-one holds ( Sum H) = ( Sum I);

        let H,I be FinSequence of V;

        assume that

         A3: ( len H) = (k + 1) and

         A4: ( rng H) = ( rng I) and

         A5: H is one-to-one and

         A6: I is one-to-one;

        (k + 1) in ( Seg (k + 1)) by FINSEQ_1: 4;

        then

         A7: (k + 1) in ( dom H) by A3, FINSEQ_1:def 3;

        then (H . (k + 1)) in ( rng I) by A4, FUNCT_1:def 3;

        then

        consider x be object such that

         A8: x in ( dom I) and

         A9: (H . (k + 1)) = (I . x) by FUNCT_1:def 3;

        reconsider v = (H . (k + 1)) as Element of V by A7, FUNCT_1: 102;

        reconsider n = x as Element of NAT by A8;

        

         A10: ( len H) = ( len I) by A4, A5, A6, FINSEQ_1: 48;

        then

         A11: x in ( Seg (k + 1)) by A3, A8, FINSEQ_1:def 3;

        then

         A12: n <= (k + 1) by FINSEQ_1: 1;

        then

        consider m2 be Nat such that

         A13: (n + m2) = (k + 1) by NAT_1: 10;

        defpred P[ Nat, object] means $2 = (I . (n + $1));

        reconsider m2 as Element of NAT by ORDINAL1:def 12;

        

         A14: for j be Nat st j in ( Seg m2) holds ex x be object st P[j, x];

        consider q2 be FinSequence such that

         A15: ( dom q2) = ( Seg m2) and

         A16: for k be Nat st k in ( Seg m2) holds P[k, (q2 . k)] from FINSEQ_1:sch 1( A14);

        

         A17: ( rng q2) c= the carrier of V

        proof

          let x be object;

          assume x in ( rng q2);

          then

          consider y be object such that

           A18: y in ( dom q2) and

           A19: x = (q2 . y) by FUNCT_1:def 3;

          reconsider y as Element of NAT by A18;

          1 <= y by A15, A18, FINSEQ_1: 1;

          then

           A20: 1 <= (n + y) by NAT_1: 12;

          y <= m2 by A15, A18, FINSEQ_1: 1;

          then (n + y) <= ( len I) by A3, A10, A13, XREAL_1: 7;

          then (n + y) in ( dom I) by A20, FINSEQ_3: 25;

          then

          reconsider xx = (I . (n + y)) as Element of V by FUNCT_1: 102;

          xx in the carrier of V;

          hence thesis by A15, A16, A18, A19;

        end;

        reconsider p = (H | ( Seg k)) as FinSequence of V by FINSEQ_1: 18;

        

         A21: p is one-to-one by A5, FUNCT_1: 52;

        ( Seg k) = (( Seg (k + 1)) \ {(k + 1)}) by FINSEQ_1: 10;

        then

         A22: (H .: ( Seg k)) = ((H .: ( Seg (k + 1))) \ ( Im (H,(k + 1)))) by A5, FUNCT_1: 64;

        

         A23: 1 <= n by A11, FINSEQ_1: 1;

        then

        consider m1 be Nat such that

         A24: (1 + m1) = n by NAT_1: 10;

        reconsider q1 = (I | ( Seg m1)) as FinSequence of V by FINSEQ_1: 18;

        reconsider q2 as FinSequence of V by A17, FINSEQ_1:def 4;

        m1 <= n by A24, NAT_1: 11;

        then

         A25: m1 <= (k + 1) by A12, XXREAL_0: 2;

        then

         A26: ( len q1) = m1 by A3, A10, FINSEQ_1: 17;

         A27:

        now

          let j be Nat;

          assume

           A28: j in ( dom q2);

          ( len (q1 ^ <*v*>)) = (m1 + ( len <*v*>)) by A26, FINSEQ_1: 22

          .= n by A24, FINSEQ_1: 39;

          hence (I . (( len (q1 ^ <*v*>)) + j)) = (q2 . j) by A15, A16, A28;

        end;

        set q = (q1 ^ q2);

        

         A29: m1 < n by A24, XREAL_1: 29;

        

         A30: {v} misses ( rng q)

        proof

          set y = the Element of ( {v} /\ ( rng q));

          assume not thesis;

          then

           A31: ( {v} /\ ( rng q)) <> {} by XBOOLE_0:def 7;

          then

           A32: y in {v} by XBOOLE_0:def 4;

           A33:

          now

            assume y in ( rng q1);

            then

            consider y1 be object such that

             A34: y1 in ( dom q1) and

             A35: y = (q1 . y1) by FUNCT_1:def 3;

            

             A36: y1 in ( Seg m1) by A3, A10, A25, A34, FINSEQ_1: 17;

            reconsider y1 as Element of NAT by A34;

            y1 <= m1 by A36, FINSEQ_1: 1;

            then

             A37: y1 <= (k + 1) by A25, XXREAL_0: 2;

            1 <= y1 by A36, FINSEQ_1: 1;

            then y1 in ( Seg (k + 1)) by A37, FINSEQ_1: 1;

            then

             A38: y1 in ( dom I) by A3, A10, FINSEQ_1:def 3;

            (q1 . y1) = (I . y1) by A34, FUNCT_1: 47;

            then

             A39: (I . y1) = (I . n) by A9, A32, A35, TARSKI:def 1;

            y1 <> n by A29, A36, FINSEQ_1: 1;

            hence contradiction by A6, A8, A38, A39;

          end;

          

           A40: y = (I . n) by A9, A32, TARSKI:def 1;

           A41:

          now

            assume y in ( rng q2);

            then

            consider y1 be object such that

             A42: y1 in ( dom q2) and

             A43: y = (q2 . y1) by FUNCT_1:def 3;

            reconsider y1 as Element of NAT by A42;

            y1 <= m2 by A15, A42, FINSEQ_1: 1;

            then

             A44: (n + y1) <= (k + 1) by A13, XREAL_1: 7;

            1 <= (n + y1) by A23, NAT_1: 12;

            then (n + y1) in ( Seg (k + 1)) by A44, FINSEQ_1: 1;

            then

             A45: (n + y1) in ( dom I) by A3, A10, FINSEQ_1:def 3;

            (I . n) = (I . (n + y1)) by A15, A16, A40, A42, A43;

            then

             A46: n = (n + y1) by A6, A8, A45;

            y1 <> 0 by A15, A42, FINSEQ_1: 1;

            hence contradiction by A46;

          end;

          y in ( rng q) by A31, XBOOLE_0:def 4;

          then y in (( rng q1) \/ ( rng q2)) by FINSEQ_1: 31;

          hence thesis by A33, A41, XBOOLE_0:def 3;

        end;

        

         A47: q is one-to-one

        proof

          let y1,y2 be object;

          assume that

           A48: y1 in ( dom q) & y2 in ( dom q) and

           A49: (q . y1) = (q . y2);

          reconsider x1 = y1, x2 = y2 as Element of NAT by A48;

           A50:

          now

            given j1 be Nat such that

             A51: j1 in ( dom q2) and

             A52: x1 = (( len q1) + j1);

            

             A53: (q2 . j1) = (I . (n + j1)) by A15, A16, A51;

            j1 <= m2 by A15, A51, FINSEQ_1: 1;

            then

             A54: (n + j1) <= (k + 1) by A13, XREAL_1: 7;

            1 <= (n + j1) by A23, NAT_1: 12;

            then (n + j1) in ( Seg (k + 1)) by A54, FINSEQ_1: 1;

            then

             A55: (n + j1) in ( dom I) by A3, A10, FINSEQ_1:def 3;

            given j2 be Nat such that

             A56: j2 in ( dom q2) and

             A57: x2 = (( len q1) + j2);

            

             A58: (q2 . j2) = (I . (n + j2)) by A15, A16, A56;

            j2 <= m2 by A15, A56, FINSEQ_1: 1;

            then

             A59: (n + j2) <= (k + 1) by A13, XREAL_1: 7;

            1 <= (n + j2) by A23, NAT_1: 12;

            then (n + j2) in ( Seg (k + 1)) by A59, FINSEQ_1: 1;

            then

             A60: (n + j2) in ( dom I) by A3, A10, FINSEQ_1:def 3;

            (q2 . j1) = (q . (m1 + j2)) by A26, A49, A51, A52, A57, FINSEQ_1:def 7

            .= (q2 . j2) by A26, A56, FINSEQ_1:def 7;

            then (n + j1) = (n + j2) by A6, A53, A58, A55, A60;

            hence thesis by A52, A57;

          end;

           A61:

          now

            assume

             A62: x2 in ( dom q1);

            then (q1 . x2) = (I . x2) by FUNCT_1: 47;

            then

             A63: (q . x2) = (I . x2) by A62, FINSEQ_1:def 7;

            

             A64: x2 in ( Seg m1) by A3, A10, A25, A62, FINSEQ_1: 17;

            then

             A65: 1 <= x2 by FINSEQ_1: 1;

            

             A66: x2 <= m1 by A64, FINSEQ_1: 1;

            then x2 <= (k + 1) by A25, XXREAL_0: 2;

            then x2 in ( Seg (k + 1)) by A65, FINSEQ_1: 1;

            then

             A67: x2 in ( dom I) by A3, A10, FINSEQ_1:def 3;

            given j be Nat such that

             A68: j in ( dom q2) and

             A69: x1 = (( len q1) + j);

            (q2 . j) = (I . (n + j)) by A15, A16, A68;

            then

             A70: (I . x2) = (I . (n + j)) by A49, A68, A69, A63, FINSEQ_1:def 7;

            j <= m2 by A15, A68, FINSEQ_1: 1;

            then

             A71: (n + j) <= (k + 1) by A13, XREAL_1: 7;

            1 <= (n + j) by A23, NAT_1: 12;

            then (n + j) in ( Seg (k + 1)) by A71, FINSEQ_1: 1;

            then

             A72: (n + j) in ( dom I) by A3, A10, FINSEQ_1:def 3;

            

             A73: n <= (n + j) by NAT_1: 12;

            x2 < n by A29, A66, XXREAL_0: 2;

            hence thesis by A6, A70, A67, A72, A73;

          end;

           A74:

          now

            assume

             A75: x1 in ( dom q1);

            then (q1 . x1) = (I . x1) by FUNCT_1: 47;

            then

             A76: (q . x1) = (I . x1) by A75, FINSEQ_1:def 7;

            

             A77: x1 in ( Seg m1) by A3, A10, A25, A75, FINSEQ_1: 17;

            then

             A78: 1 <= x1 by FINSEQ_1: 1;

            

             A79: x1 <= m1 by A77, FINSEQ_1: 1;

            then x1 <= (k + 1) by A25, XXREAL_0: 2;

            then x1 in ( Seg (k + 1)) by A78, FINSEQ_1: 1;

            then

             A80: x1 in ( dom I) by A3, A10, FINSEQ_1:def 3;

            given j be Nat such that

             A81: j in ( dom q2) and

             A82: x2 = (( len q1) + j);

            (q2 . j) = (I . (n + j)) by A15, A16, A81;

            then

             A83: (I . x1) = (I . (n + j)) by A49, A81, A82, A76, FINSEQ_1:def 7;

            j <= m2 by A15, A81, FINSEQ_1: 1;

            then

             A84: (n + j) <= (k + 1) by A13, XREAL_1: 7;

            1 <= (n + j) by A23, NAT_1: 12;

            then (n + j) in ( Seg (k + 1)) by A84, FINSEQ_1: 1;

            then

             A85: (n + j) in ( dom I) by A3, A10, FINSEQ_1:def 3;

            

             A86: n <= (n + j) by NAT_1: 12;

            x1 < n by A29, A79, XXREAL_0: 2;

            hence thesis by A6, A83, A80, A85, A86;

          end;

          

           A87: q1 is one-to-one by A6, FUNCT_1: 52;

          now

            assume

             A88: x1 in ( dom q1) & x2 in ( dom q1);

            then (q1 . x1) = (q . x1) & (q1 . x2) = (q . x2) by FINSEQ_1:def 7;

            hence thesis by A49, A87, A88;

          end;

          hence thesis by A48, A74, A61, A50, FINSEQ_1: 25;

        end;

        k <= (k + 1) by NAT_1: 12;

        then

         A89: ( len p) = k by A3, FINSEQ_1: 17;

         A90:

        now

          let k be Nat;

          assume k in ( dom <*v*>);

          then k in ( Seg 1) by FINSEQ_1: 38;

          then k = 1 by FINSEQ_1: 2, TARSKI:def 1;

          hence (H . (( len p) + k)) = ( <*v*> . k) by A89, FINSEQ_1: 40;

        end;

         A91:

        now

          let j be Nat;

          assume

           A92: j in ( dom (q1 ^ <*v*>));

           A93:

          now

            assume j in ( Seg m1);

            then

             A94: j in ( dom q1) by A3, A10, A25, FINSEQ_1: 17;

            then (q1 . j) = (I . j) by FUNCT_1: 47;

            hence (I . j) = ((q1 ^ <*v*>) . j) by A94, FINSEQ_1:def 7;

          end;

           A95:

          now

            1 in ( Seg 1) & ( len <*v*>) = 1 by FINSEQ_1: 1, FINSEQ_1: 39;

            then 1 in ( dom <*v*>) by FINSEQ_1:def 3;

            then

             A96: ((q1 ^ <*v*>) . (( len q1) + 1)) = ( <*v*> . 1) by FINSEQ_1:def 7;

            assume j in {n};

            then j = n by TARSKI:def 1;

            hence ((q1 ^ <*v*>) . j) = (I . j) by A9, A24, A26, A96, FINSEQ_1: 40;

          end;

          ( len (q1 ^ <*v*>)) = (m1 + ( len <*v*>)) by A26, FINSEQ_1: 22

          .= (m1 + 1) by FINSEQ_1: 40;

          then j in ( Seg (m1 + 1)) by A92, FINSEQ_1:def 3;

          then j in (( Seg m1) \/ {n}) by A24, FINSEQ_1: 9;

          hence (I . j) = ((q1 ^ <*v*>) . j) by A93, A95, XBOOLE_0:def 3;

        end;

        ( len q2) = m2 by A15, FINSEQ_1:def 3;

        

        then (( len (q1 ^ <*v*>)) + ( len q2)) = ((( len q1) + ( len <*v*>)) + m2) by FINSEQ_1: 22

        .= (k + 1) by A24, A13, A26, FINSEQ_1: 40;

        then ( dom I) = ( Seg (( len (q1 ^ <*v*>)) + ( len q2))) by A3, A10, FINSEQ_1:def 3;

        then

         A97: I = ((q1 ^ <*v*>) ^ q2) by A91, A27, FINSEQ_1:def 7;

        

        then ( rng I) = (( rng (q1 ^ <*v*>)) \/ ( rng q2)) by FINSEQ_1: 31

        .= ((( rng <*v*>) \/ ( rng q1)) \/ ( rng q2)) by FINSEQ_1: 31

        .= (( {v} \/ ( rng q1)) \/ ( rng q2)) by FINSEQ_1: 39

        .= ( {v} \/ (( rng q1) \/ ( rng q2))) by XBOOLE_1: 4

        .= ( {v} \/ ( rng q)) by FINSEQ_1: 31;

        then

         A98: ( rng q) = (( rng I) \ {v}) by A30, XBOOLE_1: 88;

        

         A99: ( Seg (k + 1)) = ( dom H) by A3, FINSEQ_1:def 3;

        then ( rng p) = (H .: ( Seg k)) & ( rng H) = (H .: ( Seg (k + 1))) by RELAT_1: 113, RELAT_1: 115;

        then

         A100: ( rng p) = ( rng q) by A4, A98, A99, A22, FINSEQ_1: 4, FUNCT_1: 59;

        ( len <*v*>) = 1 & for k be Nat st k in ( dom p) holds (H . k) = (p . k) by FINSEQ_1: 39, FUNCT_1: 47;

        then H = (p ^ <*v*>) by A89, A99, A90, FINSEQ_1:def 7;

        then

         A101: ( Sum H) = (( Sum p) + ( Sum <*v*>)) by Th41;

        ( Sum I) = (( Sum (q1 ^ <*v*>)) + ( Sum q2)) by A97, Th41

        .= ((( Sum q1) + ( Sum <*v*>)) + ( Sum q2)) by Th41

        .= (( Sum <*v*>) + (( Sum q1) + ( Sum q2))) by Def3

        .= (( Sum q) + ( Sum <*v*>)) by Th41;

        hence ( Sum H) = ( Sum I) by A2, A89, A100, A21, A47, A101;

      end;

      then

       A102: for k st P[k] holds P[(k + 1)];

      now

        let H,I be FinSequence of V;

        assume that

         A103: ( len H) = 0 and

         A104: ( rng H) = ( rng I) and H is one-to-one and I is one-to-one;

        H = {} by A103;

        then I = {} by A104;

        then

         A105: ( len I) = 0 ;

        ( Sum H) = ( 0. V) by A103, Lm5;

        hence ( Sum H) = ( Sum I) by A105, Lm5;

      end;

      then

       A106: P[ 0 ];

      for k holds P[k] from NAT_1:sch 2( A106, A102);

      hence thesis by A1;

    end;

    theorem :: RLVECT_1:43

    for V be non empty addLoopStr holds ( Sum ( <*> the carrier of V)) = ( 0. V) by Lm4;

    theorem :: RLVECT_1:44

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, v be Element of V holds ( Sum <*v*>) = v by Lm6;

    theorem :: RLVECT_1:45

    

     Th45: for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,u be Element of V holds ( Sum <*v, u*>) = (v + u)

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr, v,u be Element of V;

       <*v, u*> = ( <*v*> ^ <*u*>) by FINSEQ_1:def 9;

      

      hence ( Sum <*v, u*>) = (( Sum <*v*>) + ( Sum <*u*>)) by Th41

      .= (v + ( Sum <*u*>)) by Lm6

      .= (v + u) by Lm6;

    end;

    theorem :: RLVECT_1:46

    

     Th46: for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V holds ( Sum <*v, u, w*>) = ((v + u) + w)

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V;

       <*v, u, w*> = ( <*v, u*> ^ <*w*>) by FINSEQ_1: 43;

      

      hence ( Sum <*v, u, w*>) = (( Sum <*v, u*>) + ( Sum <*w*>)) by Th41

      .= (( Sum <*v, u*>) + w) by Lm6

      .= ((v + u) + w) by Th45;

    end;

    theorem :: RLVECT_1:47

    for V be RealLinearSpace, a be Real holds (a * ( Sum ( <*> the carrier of V))) = ( 0. V) by Lm4, Th10;

    theorem :: RLVECT_1:48

    for V be RealLinearSpace, a be Real, v,u be VECTOR of V holds (a * ( Sum <*v, u*>)) = ((a * v) + (a * u))

    proof

      let V be RealLinearSpace, a be Real, v,u be VECTOR of V;

      

      thus (a * ( Sum <*v, u*>)) = (a * (v + u)) by Th45

      .= ((a * v) + (a * u)) by Def5;

    end;

    theorem :: RLVECT_1:49

    for V be RealLinearSpace, a be Real, v,u,w be VECTOR of V holds (a * ( Sum <*v, u, w*>)) = (((a * v) + (a * u)) + (a * w))

    proof

      let V be RealLinearSpace, a be Real, v,u,w be VECTOR of V;

      

      thus (a * ( Sum <*v, u, w*>)) = (a * ((v + u) + w)) by Th46

      .= ((a * (v + u)) + (a * w)) by Def5

      .= (((a * v) + (a * u)) + (a * w)) by Def5;

    end;

    theorem :: RLVECT_1:50

    ( - ( Sum ( <*> the carrier of V))) = ( 0. V)

    proof

      

      thus ( - ( Sum ( <*> the carrier of V))) = ( - ( 0. V)) by Lm4

      .= ( 0. V);

    end;

    theorem :: RLVECT_1:51

    ( - ( Sum <*v*>)) = ( - v) by Lm6;

    theorem :: RLVECT_1:52

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u be Element of V holds ( - ( Sum <*v, u*>)) = (( - v) - u)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u be Element of V;

      

      thus ( - ( Sum <*v, u*>)) = ( - (v + u)) by Th45

      .= (( - v) - u) by Th30;

    end;

    theorem :: RLVECT_1:53

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V holds ( - ( Sum <*v, u, w*>)) = ((( - v) - u) - w)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V;

      

      thus ( - ( Sum <*v, u, w*>)) = ( - ((v + u) + w)) by Th46

      .= (( - (v + u)) - w) by Th30

      .= ((( - v) - u) - w) by Th30;

    end;

    theorem :: RLVECT_1:54

    

     Th54: for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V holds ( Sum <*v, w*>) = ( Sum <*w, v*>)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V;

      

      thus ( Sum <*v, w*>) = (v + w) by Th45

      .= ( Sum <*w, v*>) by Th45;

    end;

    theorem :: RLVECT_1:55

    ( Sum <*v, w*>) = (( Sum <*v*>) + ( Sum <*w*>))

    proof

      

      thus ( Sum <*v, w*>) = (v + w) by Th45

      .= (( Sum <*v*>) + w) by Lm6

      .= (( Sum <*v*>) + ( Sum <*w*>)) by Lm6;

    end;

    ::$Canceled

    theorem :: RLVECT_1:57

    ( Sum <*( 0. V), v*>) = v & ( Sum <*v, ( 0. V)*>) = v

    proof

      

      thus ( Sum <*( 0. V), v*>) = (( 0. V) + v) by Th45

      .= v;

      

      thus ( Sum <*v, ( 0. V)*>) = (v + ( 0. V)) by Th45

      .= v;

    end;

    theorem :: RLVECT_1:58

    ( Sum <*v, ( - v)*>) = ( 0. V) & ( Sum <*( - v), v*>) = ( 0. V)

    proof

      

       A1: (v + ( - v)) = ( 0. V) by Def10;

      hence ( Sum <*v, ( - v)*>) = ( 0. V) by Th45;

      (( - v) + v) = ( 0. V) by A1, Lm1;

      hence thesis by Th45;

    end;

    theorem :: RLVECT_1:59

    ( Sum <*v, ( - w)*>) = (v - w) by Th45;

    theorem :: RLVECT_1:60

    

     Th59: ( Sum <*( - v), ( - w)*>) = ( - (w + v))

    proof

      

      thus ( Sum <*( - v), ( - w)*>) = (( - v) + ( - w)) by Th45

      .= ( - (w + v)) by Lm3;

    end;

    theorem :: RLVECT_1:61

    

     Th60: for V be RealLinearSpace, v be VECTOR of V holds ( Sum <*v, v*>) = (2 * v)

    proof

      let V be RealLinearSpace, v be VECTOR of V;

      

      thus ( Sum <*v, v*>) = (v + v) by Th45

      .= ((1 * v) + v) by Def8

      .= ((1 * v) + (1 * v)) by Def8

      .= ((1 + 1) * v) by Def6

      .= (2 * v);

    end;

    theorem :: RLVECT_1:62

    for V be RealLinearSpace, v be VECTOR of V holds ( Sum <*( - v), ( - v)*>) = (( - 2) * v)

    proof

      let V be RealLinearSpace, v be VECTOR of V;

      

      thus ( Sum <*( - v), ( - v)*>) = ( - (v + v)) by Th59

      .= ( - ( Sum <*v, v*>)) by Th45

      .= ( - (2 * v)) by Th60

      .= (( - 1) * (2 * v)) by Th16

      .= ((( - 1) * 2) * v) by Def7

      .= (( - 2) * v);

    end;

    theorem :: RLVECT_1:63

    ( Sum <*u, v, w*>) = ((( Sum <*u*>) + ( Sum <*v*>)) + ( Sum <*w*>))

    proof

      

      thus ( Sum <*u, v, w*>) = ((u + v) + w) by Th46

      .= ((( Sum <*u*>) + v) + w) by Lm6

      .= ((( Sum <*u*>) + v) + ( Sum <*w*>)) by Lm6

      .= ((( Sum <*u*>) + ( Sum <*v*>)) + ( Sum <*w*>)) by Lm6;

    end;

    theorem :: RLVECT_1:64

    ( Sum <*u, v, w*>) = (( Sum <*u, v*>) + w)

    proof

      

      thus ( Sum <*u, v, w*>) = ((u + v) + w) by Th46

      .= (( Sum <*u, v*>) + w) by Th45;

    end;

    theorem :: RLVECT_1:65

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V holds ( Sum <*u, v, w*>) = (( Sum <*v, w*>) + u)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V;

      

      thus ( Sum <*u, v, w*>) = ((u + v) + w) by Th46

      .= (u + (v + w)) by Def3

      .= (( Sum <*v, w*>) + u) by Th45;

    end;

    theorem :: RLVECT_1:66

    

     Th65: for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V holds ( Sum <*u, v, w*>) = (( Sum <*u, w*>) + v)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V;

      

      thus ( Sum <*u, v, w*>) = ((u + v) + w) by Th46

      .= ((u + w) + v) by Def3

      .= (( Sum <*u, w*>) + v) by Th45;

    end;

    theorem :: RLVECT_1:67

    

     Th66: for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V holds ( Sum <*u, v, w*>) = ( Sum <*u, w, v*>)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V;

      

      thus ( Sum <*u, v, w*>) = ((u + v) + w) by Th46

      .= ((u + w) + v) by Def3

      .= ( Sum <*u, w, v*>) by Th46;

    end;

    theorem :: RLVECT_1:68

    

     Th67: for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V holds ( Sum <*u, v, w*>) = ( Sum <*v, u, w*>)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V;

      

      thus ( Sum <*u, v, w*>) = ((u + v) + w) by Th46

      .= ( Sum <*v, u, w*>) by Th46;

    end;

    theorem :: RLVECT_1:69

    

     Th68: for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V holds ( Sum <*u, v, w*>) = ( Sum <*v, w, u*>)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V;

      

      thus ( Sum <*u, v, w*>) = ( Sum <*v, u, w*>) by Th67

      .= ( Sum <*v, w, u*>) by Th66;

    end;

    theorem :: RLVECT_1:70

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V holds ( Sum <*u, v, w*>) = ( Sum <*w, v, u*>)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V;

      

      thus ( Sum <*u, v, w*>) = ( Sum <*w, u, v*>) by Th68

      .= ( Sum <*w, v, u*>) by Th66;

    end;

    ::$Canceled

    theorem :: RLVECT_1:72

    ( Sum <*( 0. V), ( 0. V), v*>) = v & ( Sum <*( 0. V), v, ( 0. V)*>) = v & ( Sum <*v, ( 0. V), ( 0. V)*>) = v

    proof

      

      thus ( Sum <*( 0. V), ( 0. V), v*>) = ((( 0. V) + ( 0. V)) + v) by Th46

      .= v;

      

      thus ( Sum <*( 0. V), v, ( 0. V)*>) = ((( 0. V) + v) + ( 0. V)) by Th46

      .= v;

      

      thus ( Sum <*v, ( 0. V), ( 0. V)*>) = (v + ( 0. V)) by Th46

      .= v;

    end;

    theorem :: RLVECT_1:73

    ( Sum <*( 0. V), u, v*>) = (u + v) & ( Sum <*u, v, ( 0. V)*>) = (u + v) & ( Sum <*u, ( 0. V), v*>) = (u + v)

    proof

      

      thus ( Sum <*( 0. V), u, v*>) = ((( 0. V) + u) + v) by Th46

      .= (u + v);

      

      thus ( Sum <*u, v, ( 0. V)*>) = ((u + v) + ( 0. V)) by Th46

      .= (u + v);

      

      thus ( Sum <*u, ( 0. V), v*>) = ((u + ( 0. V)) + v) by Th46

      .= (u + v);

    end;

    theorem :: RLVECT_1:74

    for V be RealLinearSpace, v be VECTOR of V holds ( Sum <*v, v, v*>) = (3 * v)

    proof

      let V be RealLinearSpace, v be VECTOR of V;

      

      thus ( Sum <*v, v, v*>) = (( Sum <*v, v*>) + v) by Th65

      .= ((2 * v) + v) by Th60

      .= ((2 * v) + (1 * v)) by Def8

      .= ((2 + 1) * v) by Def6

      .= (3 * v);

    end;

    theorem :: RLVECT_1:75

    ( len F) = 0 implies ( Sum F) = ( 0. V) by Lm5;

    theorem :: RLVECT_1:76

    ( len F) = 1 implies ( Sum F) = (F . 1)

    proof

      assume

       A1: ( len F) = 1;

      then ( dom F) = {1} by FINSEQ_1: 2, FINSEQ_1:def 3;

      then 1 in ( dom F) by TARSKI:def 1;

      then

       A2: (F . 1) in ( rng F) by FUNCT_1:def 3;

      ( rng F) c= the carrier of V by FINSEQ_1:def 4;

      then

      reconsider v = (F . 1) as Element of V by A2;

      F = <*v*> by A1, FINSEQ_1: 40;

      hence thesis by Lm6;

    end;

    theorem :: RLVECT_1:77

    ( len F) = 2 & v1 = (F . 1) & v2 = (F . 2) implies ( Sum F) = (v1 + v2)

    proof

      assume ( len F) = 2 & v1 = (F . 1) & v2 = (F . 2);

      then F = <*v1, v2*> by FINSEQ_1: 44;

      hence thesis by Th45;

    end;

    theorem :: RLVECT_1:78

    ( len F) = 3 & v1 = (F . 1) & v2 = (F . 2) & v = (F . 3) implies ( Sum F) = ((v1 + v2) + v)

    proof

      assume ( len F) = 3 & v1 = (F . 1) & v2 = (F . 2) & v = (F . 3);

      then F = <*v1, v2, v*> by FINSEQ_1: 45;

      hence thesis by Th46;

    end;

    begin

    definition

      let L be non empty addLoopStr;

      :: RLVECT_1:def13

      attr L is zeroed means for a be Element of L holds (a + ( 0. L)) = a & (( 0. L) + a) = a;

    end

    registration

      cluster zeroed -> right_zeroed for non empty addLoopStr;

      coherence ;

    end

    registration

      cluster Abelian right_zeroed -> zeroed for non empty addLoopStr;

      coherence

      proof

        let L be non empty addLoopStr;

        assume

         A1: L is Abelian right_zeroed;

        let a be Element of L;

        thus (a + ( 0. L)) = a by A1;

        hence thesis by A1;

      end;

      cluster Abelian right_complementable -> left_complementable for non empty addLoopStr;

      coherence

      proof

        let L be non empty addLoopStr;

        assume

         A2: L is Abelian right_complementable;

        let a be Element of L;

        consider w be Element of L such that

         A3: (a + w) = ( 0. L) by A2, ALGSTR_0:def 11;

        take w;

        thus thesis by A2, A3;

      end;

    end

    theorem :: RLVECT_1:79

    for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V holds (( - a) * v) = ( - (a * v))

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct, v be Element of V;

      

      thus (( - a) * v) = (a * ( - v)) by Th24

      .= ( - (a * v)) by Th25;

    end;

    begin

    reserve x,y for set,

k,n for Element of NAT ;

    theorem :: RLVECT_1:80

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr holds ( - ( Sum ( <*> the carrier of V))) = ( 0. V)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr;

      

      thus ( - ( Sum ( <*> the carrier of V))) = ( - ( 0. V)) by Lm4

      .= ( 0. V);

    end;

    theorem :: RLVECT_1:81

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u be Element of V holds ( - ( Sum <*v, u*>)) = (( - v) - u)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u be Element of V;

      

      thus ( - ( Sum <*v, u*>)) = ( - (v + u)) by Th45

      .= (( - v) - u) by Th30;

    end;

    theorem :: RLVECT_1:82

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V holds ( - ( Sum <*v, u, w*>)) = ((( - v) - u) - w)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u,w be Element of V;

      

      thus ( - ( Sum <*v, u, w*>)) = ( - ((v + u) + w)) by Th46

      .= (( - (v + u)) - w) by Th30

      .= ((( - v) - u) - w) by Th30;

    end;

    theorem :: RLVECT_1:83

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v be Element of V holds ( Sum <*v, ( - v)*>) = ( 0. V) & ( Sum <*( - v), v*>) = ( 0. V)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v be Element of V;

      

      thus ( Sum <*v, ( - v)*>) = (v + ( - v)) by Th45

      .= ( 0. V) by Th5;

      hence thesis by Th54;

    end;

    theorem :: RLVECT_1:84

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V holds ( Sum <*v, ( - w)*>) = (v - w) & ( Sum <*( - w), v*>) = (v - w)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V;

      thus ( Sum <*v, ( - w)*>) = (v - w) by Th45;

      hence thesis by Th54;

    end;

    theorem :: RLVECT_1:85

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V holds ( Sum <*( - v), ( - w)*>) = ( - (v + w)) & ( Sum <*( - w), ( - v)*>) = ( - (v + w))

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,w be Element of V;

      

      thus ( Sum <*( - v), ( - w)*>) = (( - v) + ( - w)) by Th45

      .= ( - (v + w)) by Lm3;

      hence thesis by Th54;

    end;