rlvect_2.miz



    begin

    reserve x,y,y1,y2 for set,

p for FinSequence,

i,k,l,n for Nat,

V for RealLinearSpace,

u,v,v1,v2,v3,w for VECTOR of V,

a,b for Real,

F,G,H1,H2 for FinSequence of V,

A,B for Subset of V,

f for Function of the carrier of V, REAL ;

    definition

      let S be 1-sorted;

      let x;

      assume

       A1: x in S;

      :: RLVECT_2:def1

      func vector (S,x) -> Element of S equals

      : Def1: x;

      coherence by A1;

    end

    theorem :: RLVECT_2:1

    for S be non empty 1-sorted, v be Element of S holds ( vector (S,v)) = v by Def1, RLVECT_1: 1;

    theorem :: RLVECT_2:2

    

     Th2: for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, F,G,H be FinSequence of the carrier of V st ( len F) = ( len G) & ( len F) = ( len H) & for k st k in ( dom F) holds (H . k) = ((F /. k) + (G /. k)) holds ( Sum H) = (( Sum F) + ( Sum G))

    proof

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

      defpred P[ Nat] means for F,G,H be FinSequence of the carrier of V st ( len F) = $1 & ( len F) = ( len G) & ( len F) = ( len H) & (for k st k in ( dom F) holds (H . k) = ((F /. k) + (G /. k))) holds ( Sum H) = (( Sum F) + ( Sum G));

      now

        let k;

        assume

         A1: for F,G,H be FinSequence of the carrier of V st ( len F) = k & ( len F) = ( len G) & ( len F) = ( len H) & (for k st k in ( dom F) holds (H . k) = ((F /. k) + (G /. k))) holds ( Sum H) = (( Sum F) + ( Sum G));

        let F,G,H be FinSequence of the carrier of V;

        assume that

         A2: ( len F) = (k + 1) and

         A3: ( len F) = ( len G) and

         A4: ( len F) = ( len H) and

         A5: for k st k in ( dom F) holds (H . k) = ((F /. k) + (G /. k));

        reconsider f = (F | ( Seg k)), g = (G | ( Seg k)), h = (H | ( Seg k)) as FinSequence of the carrier of V by FINSEQ_1: 18;

        

         A6: ( len h) = k by A2, A4, FINSEQ_3: 53;

        

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

        then

         A8: (k + 1) in ( dom G) by A2, A3, FINSEQ_1:def 3;

        then

         A9: (G . (k + 1)) in ( rng G) by FUNCT_1:def 3;

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

        then

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

        

         A11: (k + 1) in ( dom F) by A2, A7, FINSEQ_1:def 3;

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

        then

        reconsider v = (F . (k + 1)), u = (G . (k + 1)), w = (H . (k + 1)) as Element of V by A9, A10;

        

         A12: w = ((F /. (k + 1)) + (G /. (k + 1))) by A5, A11

        .= (v + (G /. (k + 1))) by A11, PARTFUN1:def 6

        .= (v + u) by A8, PARTFUN1:def 6;

        G = (g ^ <*u*>) by A2, A3, FINSEQ_3: 55;

        then

         A13: ( Sum G) = (( Sum g) + ( Sum <*u*>)) by RLVECT_1: 41;

        

         A14: ( Sum <*v*>) = v by RLVECT_1: 44;

        

         A15: ( len f) = k by A2, FINSEQ_3: 53;

        

         A16: ( len g) = k by A2, A3, FINSEQ_3: 53;

        now

          let i;

          assume

           A17: i in ( dom f);

          then

           A18: (F . i) = (f . i) by FUNCT_1: 47;

          ( len f) <= ( len F) by A2, A15, NAT_1: 12;

          then

           A19: ( dom f) c= ( dom F) by FINSEQ_3: 30;

          then i in ( dom F) by A17;

          then i in ( dom G) by A3, FINSEQ_3: 29;

          then

           A20: (G /. i) = (G . i) by PARTFUN1:def 6;

          i in ( dom h) by A15, A6, A17, FINSEQ_3: 29;

          then

           A21: (H . i) = (h . i) by FUNCT_1: 47;

          (F /. i) = (F . i) by A17, A19, PARTFUN1:def 6;

          then

           A22: (f /. i) = (F /. i) by A17, A18, PARTFUN1:def 6;

          

           A23: i in ( dom g) by A15, A16, A17, FINSEQ_3: 29;

          then (G . i) = (g . i) by FUNCT_1: 47;

          then (g /. i) = (G /. i) by A23, A20, PARTFUN1:def 6;

          hence (h . i) = ((f /. i) + (g /. i)) by A5, A17, A21, A19, A22;

        end;

        then

         A24: ( Sum h) = (( Sum f) + ( Sum g)) by A1, A15, A16, A6;

        F = (f ^ <*v*>) by A2, FINSEQ_3: 55;

        then

         A25: ( Sum F) = (( Sum f) + ( Sum <*v*>)) by RLVECT_1: 41;

        

         A26: ( Sum <*u*>) = u by RLVECT_1: 44;

        H = (h ^ <*w*>) by A2, A4, FINSEQ_3: 55;

        

        hence ( Sum H) = (( Sum h) + ( Sum <*w*>)) by RLVECT_1: 41

        .= ((( Sum f) + ( Sum g)) + (v + u)) by A24, A12, RLVECT_1: 44

        .= (((( Sum f) + ( Sum g)) + v) + u) by RLVECT_1:def 3

        .= ((( Sum F) + ( Sum g)) + u) by A25, A14, RLVECT_1:def 3

        .= (( Sum F) + ( Sum G)) by A13, A26, RLVECT_1:def 3;

      end;

      then

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

      

       A28: P[ 0 ]

      proof

        let F,G,H be FinSequence of the carrier of V;

        assume that

         A29: ( len F) = 0 and

         A30: ( len F) = ( len G) and

         A31: ( len F) = ( len H);

        

         A32: ( Sum H) = ( 0. V) by A29, A31, RLVECT_1: 75;

        ( Sum F) = ( 0. V) & ( Sum G) = ( 0. V) by A29, A30, RLVECT_1: 75;

        hence thesis by A32;

      end;

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

      hence thesis;

    end;

    theorem :: RLVECT_2:3

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

    proof

      assume that

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

       A2: for k st k in ( dom F) holds (G . k) = (a * (F /. k));

      

       A3: ( dom F) = ( Seg ( len F)) & ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3;

      now

        let k be Nat, v;

        assume that

         A4: k in ( dom G) and

         A5: v = (F . k);

        v = (F /. k) by A1, A3, A4, A5, PARTFUN1:def 6;

        hence (G . k) = (a * v) by A1, A2, A3, A4;

      end;

      hence thesis by A1, RLVECT_1: 39;

    end;

    theorem :: RLVECT_2:4

    

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

    proof

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

      assume that

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

       A2: for k st k in ( dom F) holds (G . k) = ( - (F /. k));

      now

        let k be Nat;

        let v be Element of V;

        assume that

         A3: k in ( dom G) and

         A4: v = (F . k);

        

         A5: ( dom G) = ( Seg ( len G)) & ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3;

        then v = (F /. k) by A1, A3, A4, PARTFUN1:def 6;

        hence (G . k) = ( - v) by A1, A2, A3, A5;

      end;

      hence thesis by A1, RLVECT_1: 40;

    end;

    theorem :: RLVECT_2:5

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

    proof

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

      assume that

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

       A2: ( len F) = ( len H) and

       A3: for k st k in ( dom F) holds (H . k) = ((F /. k) - (G /. k));

      deffunc Q( set) = ( - (G /. $1));

      consider I be FinSequence such that

       A4: ( len I) = ( len G) and

       A5: for k be Nat st k in ( dom I) holds (I . k) = Q(k) from FINSEQ_1:sch 2;

      ( dom I) = ( Seg ( len G)) by A4, FINSEQ_1:def 3;

      then

       A6: ( dom G) = ( Seg ( len G)) & for k st k in ( Seg ( len G)) holds (I . k) = Q(k) by A5, FINSEQ_1:def 3;

      ( rng I) c= the carrier of V

      proof

        let x be object;

        assume x in ( rng I);

        then

        consider y be object such that

         A7: y in ( dom I) and

         A8: (I . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A7;

        x = ( - (G /. y)) by A5, A7, A8;

        then

        reconsider v = x as Element of V;

        v in V;

        hence thesis;

      end;

      then

      reconsider I as FinSequence of the carrier of V by FINSEQ_1:def 4;

       A9:

      now

        let k;

        assume

         A10: k in ( dom F);

        

         A11: ( dom F) = ( Seg ( len F)) & ( dom I) = ( Seg ( len I)) by FINSEQ_1:def 3;

        then

         A12: (I . k) = (I /. k) by A1, A4, A10, PARTFUN1:def 6;

        

        thus (H . k) = ((F /. k) - (G /. k)) by A3, A10

        .= ((F /. k) + (I /. k)) by A1, A4, A5, A11, A10, A12;

      end;

      ( Sum I) = ( - ( Sum G)) by A4, A6, Th4;

      hence thesis by A1, A2, A4, A9, Th2;

    end;

    theorem :: RLVECT_2:6

    

     Th6: for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, F,G be FinSequence of the carrier of V holds for f be Permutation of ( dom F) st ( len F) = ( len G) & (for i st i in ( dom G) holds (G . i) = (F . (f . i))) holds ( Sum F) = ( Sum G)

    proof

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

      let f be Permutation of ( dom F);

      defpred P[ Nat] means for H1,H2 be FinSequence of the carrier of V st ( len H1) = $1 & ( len H1) = ( len H2) holds for f be Permutation of ( dom H1) st (for i st i in ( dom H2) holds (H2 . i) = (H1 . (f . i))) holds ( Sum H1) = ( Sum H2);

      now

        let k;

        assume

         A1: for H1,H2 be FinSequence of the carrier of V st ( len H1) = k & ( len H1) = ( len H2) holds for f be Permutation of ( dom H1) st (for i st i in ( dom H2) holds (H2 . i) = (H1 . (f . i))) holds ( Sum H1) = ( Sum H2);

        let H1,H2 be FinSequence of the carrier of V;

        assume that

         A2: ( len H1) = (k + 1) and

         A3: ( len H1) = ( len H2);

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

        let f be Permutation of ( dom H1);

        

         A4: ( dom H1) = ( Seg (k + 1)) by A2, FINSEQ_1:def 3;

        then

         A5: ( rng f) = ( Seg (k + 1)) by FUNCT_2:def 3;

         A6:

        now

          let n;

          assume n in ( dom f);

          then (f . n) in ( Seg (k + 1)) by A5, FUNCT_1:def 3;

          hence (f . n) is Element of NAT ;

        end;

        

         A7: ( dom H2) = ( Seg (k + 1)) by A2, A3, FINSEQ_1:def 3;

        then

        reconsider v = (H2 . (k + 1)) as Element of V by FINSEQ_1: 4, FUNCT_1: 102;

        

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

        ( Seg (k + 1)) = {} implies ( Seg (k + 1)) = {} ;

        then

         A9: ( dom f) = ( Seg (k + 1)) by A4, FUNCT_2:def 1;

        

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

        then

         A11: (f . (k + 1)) in ( Seg (k + 1)) by A9, A5, FUNCT_1:def 3;

        then

        reconsider n = (f . (k + 1)) as Element of NAT ;

        

         A12: n <= (k + 1) by A11, 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 = (H1 . (n + $1));

        1 <= n by A11, FINSEQ_1: 1;

        then

        consider m1 be Nat such that

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

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

        

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

        consider q2 be FinSequence such that

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

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

        ( 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 A16, A18, FINSEQ_1: 1;

          then

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

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

          then (n + y) <= ( len H1) by A2, A13, XREAL_1: 7;

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

          then

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

          xx in the carrier of V;

          hence thesis by A16, A17, A18, A19;

        end;

        then

        reconsider q2 as FinSequence of the carrier of V by FINSEQ_1:def 4;

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

        defpred P[ set, object] means ((f . $1) in ( dom q1) implies $2 = (f . $1)) & ( not (f . $1) in ( dom q1) implies for l st l = (f . $1) holds $2 = (l - 1));

        

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

        then

         A22: ( Seg k) c= ( Seg (k + 1)) by FINSEQ_1: 5;

        

         A23: for i be Nat st i in ( Seg k) holds ex y be object st P[i, y]

        proof

          let i be Nat;

          assume

           A24: i in ( Seg k);

          now

            (f . i) in ( Seg (k + 1)) by A9, A5, A22, A24, FUNCT_1:def 3;

            then

            reconsider j = (f . i) as Element of NAT ;

            assume

             A25: not (f . i) in ( dom q1);

            take y = (j - 1);

            thus (f . i) in ( dom q1) implies y = (f . i) by A25;

            assume not (f . i) in ( dom q1);

            let t be Nat;

            assume t = (f . i);

            hence y = (t - 1);

          end;

          hence thesis;

        end;

        consider g be FinSequence such that

         A26: ( dom g) = ( Seg k) and

         A27: for i be Nat st i in ( Seg k) holds P[i, (g . i)] from FINSEQ_1:sch 1( A23);

        

         A28: ( dom p) = ( Seg k) by A2, A3, A21, FINSEQ_1: 17;

        m1 <= n by A14, NAT_1: 11;

        then

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

        then

         A30: ( dom q1) = ( Seg m1) by A2, FINSEQ_1: 17;

         A31:

        now

          let i, l;

          assume that

           A32: l = (f . i) and

           A33: not (f . i) in ( dom q1) and

           A34: i in ( dom g);

          

           A35: l < 1 or m1 < l by A30, A32, A33, FINSEQ_1: 1;

           A36:

          now

            assume (m1 + 1) = l;

            then (k + 1) = i by A10, A9, A14, A22, A26, A32, A34, FUNCT_1:def 4;

            then (k + 1) <= (k + 0 ) by A26, A34, FINSEQ_1: 1;

            hence contradiction by XREAL_1: 6;

          end;

          (f . i) in ( rng f) by A9, A22, A26, A34, FUNCT_1:def 3;

          then (m1 + 1) <= l by A4, A32, A35, FINSEQ_1: 1, NAT_1: 13;

          then (m1 + 1) < l by A36, XXREAL_0: 1;

          then ((m1 + 1) + 1) <= l by NAT_1: 13;

          hence (m1 + 2) <= l;

        end;

        

         A37: ( len q1) = m1 by A2, A29, FINSEQ_1: 17;

         A38:

        now

          let j be Nat;

          assume

           A39: j in ( dom q2);

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

          .= n by A14, FINSEQ_1: 39;

          hence (H1 . (( len (q1 ^ <*v*>)) + j)) = (q2 . j) by A16, A17, A39;

        end;

        (1 + k) = (1 + (m1 + m2)) by A14, A13;

        then

         A40: m1 <= k by NAT_1: 11;

        

         A41: ( rng g) c= ( dom p)

        proof

          let y be object;

          assume y in ( rng g);

          then

          consider x be object such that

           A42: x in ( dom g) and

           A43: (g . x) = y by FUNCT_1:def 3;

          reconsider x as Element of NAT by A42;

          now

            per cases ;

              suppose

               A44: (f . x) in ( dom q1);

              

               A45: ( dom q1) c= ( dom p) by A40, A30, A28, FINSEQ_1: 5;

              (f . x) = (g . x) by A26, A27, A42, A44;

              hence thesis by A43, A44, A45;

            end;

              suppose

               A46: not (f . x) in ( dom q1);

              reconsider j = (f . x) as Element of NAT by A9, A22, A6, A26, A42;

              

               A47: (f . x) in ( Seg (k + 1)) by A9, A5, A22, A26, A42, FUNCT_1:def 3;

              j < 1 or m1 < j by A30, A46, FINSEQ_1: 1;

              then

              reconsider l = (j - 1) as Element of NAT by A47, FINSEQ_1: 1, NAT_1: 20;

              j <= (k + 1) by A47, FINSEQ_1: 1;

              then

               A48: l <= ((k + 1) - 1) by XREAL_1: 9;

              (m1 + 2) <= j by A31, A42, A46;

              then

               A49: ((m1 + 2) - 1) <= l by XREAL_1: 9;

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

              then

               A50: 1 <= l by A49, XXREAL_0: 2;

              (g . x) = (j - 1) by A26, A27, A42, A46;

              hence thesis by A28, A43, A50, A48, FINSEQ_1: 1;

            end;

          end;

          hence thesis;

        end;

        set q = (q1 ^ q2);

        

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

        then

         A52: ( len q) = (m1 + m2) by A37, FINSEQ_1: 22;

        then

         A53: ( dom q) = ( Seg k) by A14, A13, FINSEQ_1:def 3;

        then

        reconsider g as Function of ( dom q), ( dom q) by A28, A26, A41, FUNCT_2: 2;

        

         A54: ( len p) = k by A2, A3, A21, FINSEQ_1: 17;

        

         A55: ( rng g) = ( dom q)

        proof

          thus ( rng g) c= ( dom q);

          let y be object;

          assume

           A56: y in ( dom q);

          then

          reconsider j = y as Element of NAT ;

          consider x be object such that

           A57: x in ( dom f) and

           A58: (f . x) = y by A5, A22, A53, A56, FUNCT_1:def 3;

          reconsider x as Element of NAT by A9, A57;

          now

            per cases ;

              suppose

               A59: x in ( dom g);

              now

                per cases ;

                  suppose (f . x) in ( dom q1);

                  then (g . x) = (f . x) by A26, A27, A59;

                  hence thesis by A58, A59, FUNCT_1:def 3;

                end;

                  suppose

                   A60: not (f . x) in ( dom q1);

                  j <= k by A53, A56, FINSEQ_1: 1;

                  then 1 <= (j + 1) & (j + 1) <= (k + 1) by NAT_1: 12, XREAL_1: 7;

                  then (j + 1) in ( rng f) by A5, FINSEQ_1: 1;

                  then

                  consider x1 be object such that

                   A61: x1 in ( dom f) and

                   A62: (f . x1) = (j + 1) by FUNCT_1:def 3;

                   A63:

                  now

                    assume not x1 in ( dom g);

                    then x1 in (( Seg (k + 1)) \ ( Seg k)) by A4, A26, A61, XBOOLE_0:def 5;

                    then x1 in {(k + 1)} by FINSEQ_3: 15;

                    then

                     A64: (j + 1) = (m1 + 1) by A14, A62, TARSKI:def 1;

                    1 <= j by A53, A56, FINSEQ_1: 1;

                    hence contradiction by A30, A58, A60, A64, FINSEQ_1: 1;

                  end;

                  j < 1 or m1 < j by A30, A58, A60, FINSEQ_1: 1;

                  then not (j + 1) <= m1 by A53, A56, FINSEQ_1: 1, NAT_1: 13;

                  then not (f . x1) in ( dom q1) by A30, A62, FINSEQ_1: 1;

                  

                  then (g . x1) = ((j + 1) - 1) by A26, A27, A62, A63

                  .= y;

                  hence thesis by A63, FUNCT_1:def 3;

                end;

              end;

              hence thesis;

            end;

              suppose

               A65: not x in ( dom g);

              j <= k by A53, A56, FINSEQ_1: 1;

              then 1 <= (j + 1) & (j + 1) <= (k + 1) by NAT_1: 12, XREAL_1: 7;

              then (j + 1) in ( rng f) by A5, FINSEQ_1: 1;

              then

              consider x1 be object such that

               A66: x1 in ( dom f) and

               A67: (f . x1) = (j + 1) by FUNCT_1:def 3;

              x in (( Seg (k + 1)) \ ( Seg k)) by A4, A26, A57, A65, XBOOLE_0:def 5;

              then x in {(k + 1)} by FINSEQ_3: 15;

              then

               A68: x = (k + 1) by TARSKI:def 1;

               A69:

              now

                assume not x1 in ( dom g);

                then x1 in (( Seg (k + 1)) \ ( Seg k)) by A4, A26, A66, XBOOLE_0:def 5;

                then x1 in {(k + 1)} by FINSEQ_3: 15;

                then (j + 1) = (j + 0 ) by A58, A68, A67, TARSKI:def 1;

                hence contradiction;

              end;

              m1 <= j by A14, A58, A68, XREAL_1: 29;

              then not (j + 1) <= m1 by NAT_1: 13;

              then not (f . x1) in ( dom q1) by A30, A67, FINSEQ_1: 1;

              

              then (g . x1) = ((j + 1) - 1) by A26, A27, A67, A69

              .= y;

              hence thesis by A69, FUNCT_1:def 3;

            end;

          end;

          hence thesis;

        end;

        assume

         A70: for i st i in ( dom H2) holds (H2 . i) = (H1 . (f . i));

        then

         A71: (H2 . (k + 1)) = (H1 . (f . (k + 1))) by A7, FINSEQ_1: 4;

         A72:

        now

          let j be Nat;

          assume

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

           A74:

          now

            assume j in ( Seg m1);

            then

             A75: j in ( dom q1) by A2, A29, FINSEQ_1: 17;

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

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

          end;

           A76:

          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

             A77: ((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) = (H1 . j) by A71, A14, A37, A77, FINSEQ_1: 40;

          end;

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

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

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

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

          hence (H1 . j) = ((q1 ^ <*v*>) . j) by A74, A76, XBOOLE_0:def 3;

        end;

        g is one-to-one

        proof

          let y1,y2 be object;

          assume that

           A78: y1 in ( dom g) and

           A79: y2 in ( dom g) and

           A80: (g . y1) = (g . y2);

          reconsider j1 = y1, j2 = y2 as Element of NAT by A26, A78, A79;

          

           A81: (f . y2) in ( Seg (k + 1)) by A9, A5, A22, A26, A79, FUNCT_1:def 3;

          

           A82: (f . y1) in ( Seg (k + 1)) by A9, A5, A22, A26, A78, FUNCT_1:def 3;

          then

          reconsider a = (f . y1), b = (f . y2) as Element of NAT by A81;

          now

            per cases ;

              suppose (f . y1) in ( dom q1) & (f . y2) in ( dom q1);

              then (g . j1) = (f . y1) & (g . j2) = (f . y2) by A26, A27, A78, A79;

              hence thesis by A9, A22, A26, A78, A79, A80, FUNCT_1:def 4;

            end;

              suppose

               A83: (f . y1) in ( dom q1) & not (f . y2) in ( dom q1);

              then

               A84: a <= m1 by A30, FINSEQ_1: 1;

              (g . j1) = a & (g . j2) = (b - 1) by A26, A27, A78, A79, A83;

              then

               A85: ((b - 1) + 1) <= (m1 + 1) by A80, A84, XREAL_1: 6;

              1 <= b by A81, FINSEQ_1: 1;

              then

               A86: b in ( Seg (m1 + 1)) by A85, FINSEQ_1: 1;

               not b in ( Seg m1) by A2, A29, A83, FINSEQ_1: 17;

              then b in (( Seg (m1 + 1)) \ ( Seg m1)) by A86, XBOOLE_0:def 5;

              then b in {(m1 + 1)} by FINSEQ_3: 15;

              then b = (m1 + 1) by TARSKI:def 1;

              then y2 = (k + 1) by A10, A9, A14, A22, A26, A79, FUNCT_1:def 4;

              hence thesis by A26, A79, FINSEQ_3: 8;

            end;

              suppose

               A87: not (f . y1) in ( dom q1) & (f . y2) in ( dom q1);

              then

               A88: b <= m1 by A30, FINSEQ_1: 1;

              (g . j1) = (a - 1) & (g . j2) = b by A26, A27, A78, A79, A87;

              then

               A89: ((a - 1) + 1) <= (m1 + 1) by A80, A88, XREAL_1: 6;

              1 <= a by A82, FINSEQ_1: 1;

              then

               A90: a in ( Seg (m1 + 1)) by A89, FINSEQ_1: 1;

               not a in ( Seg m1) by A2, A29, A87, FINSEQ_1: 17;

              then a in (( Seg (m1 + 1)) \ ( Seg m1)) by A90, XBOOLE_0:def 5;

              then a in {(m1 + 1)} by FINSEQ_3: 15;

              then a = (m1 + 1) by TARSKI:def 1;

              then y1 = (k + 1) by A10, A9, A14, A22, A26, A78, FUNCT_1:def 4;

              hence thesis by A26, A78, FINSEQ_3: 8;

            end;

              suppose

               A91: not (f . y1) in ( dom q1) & not (f . y2) in ( dom q1);

              then (g . j2) = (b - 1) by A26, A27, A79;

              then

               A92: (g . y2) = (b + ( - 1));

              (g . j1) = (a - 1) by A26, A27, A78, A91;

              then (g . j1) = (a + ( - 1));

              then a = b by A80, A92, XCMPLX_1: 2;

              hence thesis by A9, A22, A26, A78, A79, FUNCT_1:def 4;

            end;

          end;

          hence thesis;

        end;

        then

        reconsider g as Permutation of ( dom q) by A55, FUNCT_2: 57;

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

        .= (k + 1) by A14, A13, A37, FINSEQ_1: 40;

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

        then

         A93: H1 = ((q1 ^ <*v*>) ^ q2) by A72, A38, FINSEQ_1:def 7;

        now

          let i;

          assume

           A94: i in ( dom p);

          then (f . i) in ( rng f) by A9, A22, A28, FUNCT_1:def 3;

          then

          reconsider j = (f . i) as Element of NAT by A5;

          now

            per cases ;

              suppose

               A95: (f . i) in ( dom q1);

              then

               A96: (f . i) = (g . i) & (H1 . j) = (q1 . j) by A28, A27, A94, FUNCT_1: 47;

              (H2 . i) = (p . i) & (H2 . i) = (H1 . (f . i)) by A70, A7, A22, A28, A94, FUNCT_1: 47;

              hence (p . i) = (q . (g . i)) by A95, A96, FINSEQ_1:def 7;

            end;

              suppose

               A97: not (f . i) in ( dom q1);

              then (m1 + 2) <= j by A28, A26, A31, A94;

              then

               A98: ((m1 + 2) - 1) <= (j - 1) by XREAL_1: 9;

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

              then

               A99: m1 < (j - 1) by A98, XXREAL_0: 2;

              then m1 < j by XREAL_1: 146, XXREAL_0: 2;

              then

              reconsider j1 = (j - 1) as Element of NAT by NAT_1: 20;

              

               A100: not j1 in ( dom q1) by A30, A99, FINSEQ_1: 1;

              

               A101: (g . i) = (j - 1) by A28, A27, A94, A97;

              then (j - 1) in ( dom q) by A28, A26, A55, A94, FUNCT_1:def 3;

              then

              consider a be Nat such that

               A102: a in ( dom q2) and

               A103: j1 = (( len q1) + a) by A100, FINSEQ_1: 25;

              

               A104: ( len <*v*>) = 1 by FINSEQ_1: 39;

              

               A105: (H2 . i) = (p . i) & (H2 . i) = (H1 . (f . i)) by A70, A7, A22, A28, A94, FUNCT_1: 47;

              

               A106: H1 = (q1 ^ ( <*v*> ^ q2)) by A93, FINSEQ_1: 32;

              j in ( dom H1) by A4, A9, A5, A22, A28, A94, FUNCT_1:def 3;

              then

              consider b be Nat such that

               A107: b in ( dom ( <*v*> ^ q2)) and

               A108: j = (( len q1) + b) by A97, A106, FINSEQ_1: 25;

              

               A109: (H1 . j) = (( <*v*> ^ q2) . b) by A106, A107, A108, FINSEQ_1:def 7;

              

               A110: b = (1 + a) by A103, A108;

              (q . (j - 1)) = (q2 . a) by A102, A103, FINSEQ_1:def 7;

              hence (p . i) = (q . (g . i)) by A101, A105, A102, A109, A110, A104, FINSEQ_1:def 7;

            end;

          end;

          hence (p . i) = (q . (g . i));

        end;

        then ( Sum p) = ( Sum q) by A1, A14, A13, A54, A52;

        

        then ( Sum H2) = (( Sum q) + ( Sum <*v*>)) by A2, A3, A54, A8, RLVECT_1: 38, RLVECT_1: 44

        .= ((( Sum q1) + ( Sum q2)) + ( Sum <*v*>)) by RLVECT_1: 41

        .= (( Sum q1) + (( Sum <*v*>) + ( Sum q2))) by RLVECT_1:def 3

        .= (( Sum q1) + ( Sum ( <*v*> ^ q2))) by RLVECT_1: 41

        .= ( Sum (q1 ^ ( <*v*> ^ q2))) by RLVECT_1: 41

        .= ( Sum H1) by A93, FINSEQ_1: 32;

        hence ( Sum H1) = ( Sum H2);

      end;

      then

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

      

       A112: P[ 0 ]

      proof

        let H1,H2 be FinSequence of the carrier of V;

        assume that

         A113: ( len H1) = 0 and

         A114: ( len H1) = ( len H2);

        ( Sum H1) = ( 0. V) by A113, RLVECT_1: 75;

        hence thesis by A113, A114, RLVECT_1: 75;

      end;

      for k holds P[k] from NAT_1:sch 2( A112, A111);

      hence thesis;

    end;

    theorem :: RLVECT_2:7

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, F,G be FinSequence of the carrier of V holds for f be Permutation of ( dom F) st G = (F * f) holds ( Sum F) = ( Sum G)

    proof

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

      let f be Permutation of ( dom F);

      assume G = (F * f);

      then ( len F) = ( len G) & for i st i in ( dom G) holds (G . i) = (F . (f . i)) by FINSEQ_2: 44, FUNCT_1: 12;

      hence thesis by Th6;

    end;

    definition

      let V be non empty addLoopStr, T be finite Subset of V;

      assume

       A1: V is Abelian add-associative right_zeroed;

      :: RLVECT_2:def2

      func Sum (T) -> Element of V means

      : Def2: ex F be FinSequence of the carrier of V st ( rng F) = T & F is one-to-one & it = ( Sum F);

      existence

      proof

        consider p such that

         A2: ( rng p) = T and

         A3: p is one-to-one by FINSEQ_4: 58;

        reconsider p as FinSequence of the carrier of V by A2, FINSEQ_1:def 4;

        take ( Sum p);

        take p;

        thus thesis by A2, A3;

      end;

      uniqueness by A1, RLVECT_1: 42;

    end

    theorem :: RLVECT_2:8

    

     Th8: for V be Abelian add-associative right_zeroed non empty addLoopStr holds ( Sum ( {} V)) = ( 0. V)

    proof

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

      ( Sum ( <*> the carrier of V)) = ( 0. V) by RLVECT_1: 43;

      hence thesis by Def2, RELAT_1: 38;

    end;

    theorem :: RLVECT_2:9

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

    proof

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

      

       A1: ( Sum <*v*>) = v by RLVECT_1: 44;

      ( rng <*v*>) = {v} & <*v*> is one-to-one by FINSEQ_1: 39, FINSEQ_3: 93;

      hence thesis by A1, Def2;

    end;

    theorem :: RLVECT_2:10

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v1,v2 be Element of V holds v1 <> v2 implies ( Sum {v1, v2}) = (v1 + v2)

    proof

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

      assume v1 <> v2;

      then

       A1: <*v1, v2*> is one-to-one by FINSEQ_3: 94;

      ( rng <*v1, v2*>) = {v1, v2} & ( Sum <*v1, v2*>) = (v1 + v2) by FINSEQ_2: 127, RLVECT_1: 45;

      hence thesis by A1, Def2;

    end;

    theorem :: RLVECT_2:11

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v1,v2,v3 be Element of V holds v1 <> v2 & v2 <> v3 & v1 <> v3 implies ( Sum {v1, v2, v3}) = ((v1 + v2) + v3)

    proof

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

      assume v1 <> v2 & v2 <> v3 & v1 <> v3;

      then

       A1: <*v1, v2, v3*> is one-to-one by FINSEQ_3: 95;

      ( rng <*v1, v2, v3*>) = {v1, v2, v3} & ( Sum <*v1, v2, v3*>) = ((v1 + v2) + v3) by FINSEQ_2: 128, RLVECT_1: 46;

      hence thesis by A1, Def2;

    end;

    theorem :: RLVECT_2:12

    

     Th12: for V be Abelian add-associative right_zeroed non empty addLoopStr, S,T be finite Subset of V holds T misses S implies ( Sum (T \/ S)) = (( Sum T) + ( Sum S))

    proof

      let V be Abelian add-associative right_zeroed non empty addLoopStr, S,T be finite Subset of V;

      consider F be FinSequence of the carrier of V such that

       A1: ( rng F) = (T \/ S) and

       A2: F is one-to-one & ( Sum (T \/ S)) = ( Sum F) by Def2;

      consider G be FinSequence of the carrier of V such that

       A3: ( rng G) = T and

       A4: G is one-to-one and

       A5: ( Sum T) = ( Sum G) by Def2;

      consider H be FinSequence of the carrier of V such that

       A6: ( rng H) = S and

       A7: H is one-to-one and

       A8: ( Sum S) = ( Sum H) by Def2;

      set I = (G ^ H);

      assume T misses S;

      then

       A9: I is one-to-one by A3, A4, A6, A7, FINSEQ_3: 91;

      ( rng I) = ( rng F) by A1, A3, A6, FINSEQ_1: 31;

      

      hence ( Sum (T \/ S)) = ( Sum I) by A2, A9, RLVECT_1: 42

      .= (( Sum T) + ( Sum S)) by A5, A8, RLVECT_1: 41;

    end;

    theorem :: RLVECT_2:13

    

     Th13: for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, S,T be finite Subset of V holds ( Sum (T \/ S)) = ((( Sum T) + ( Sum S)) - ( Sum (T /\ S)))

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, S,T be finite Subset of V;

      set A = (S \ T);

      set B = (T \ S);

      set Z = (A \/ B);

      set I = (T /\ S);

      

       A1: (A \/ I) = S by XBOOLE_1: 51;

      

       A2: (B \/ I) = T by XBOOLE_1: 51;

      

       A3: Z = (T \+\ S);

      then (Z \/ I) = (T \/ S) by XBOOLE_1: 93;

      

      then (( Sum (T \/ S)) + ( Sum I)) = ((( Sum Z) + ( Sum I)) + ( Sum I)) by A3, Th12, XBOOLE_1: 103

      .= (((( Sum A) + ( Sum B)) + ( Sum I)) + ( Sum I)) by Th12, XBOOLE_1: 82

      .= ((( Sum A) + (( Sum I) + ( Sum B))) + ( Sum I)) by RLVECT_1:def 3

      .= ((( Sum A) + ( Sum I)) + (( Sum B) + ( Sum I))) by RLVECT_1:def 3

      .= (( Sum S) + (( Sum B) + ( Sum I))) by A1, Th12, XBOOLE_1: 89

      .= (( Sum T) + ( Sum S)) by A2, Th12, XBOOLE_1: 89;

      hence thesis by RLSUB_2: 61;

    end;

    theorem :: RLVECT_2:14

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, S,T be finite Subset of V holds ( Sum (T /\ S)) = ((( Sum T) + ( Sum S)) - ( Sum (T \/ S)))

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, S,T be finite Subset of V;

      ( Sum (T \/ S)) = ((( Sum T) + ( Sum S)) - ( Sum (T /\ S))) by Th13;

      then (( Sum T) + ( Sum S)) = (( Sum (T /\ S)) + ( Sum (T \/ S))) by RLSUB_2: 61;

      hence thesis by RLSUB_2: 61;

    end;

    theorem :: RLVECT_2:15

    

     Th15: for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, S,T be finite Subset of V holds ( Sum (T \ S)) = (( Sum (T \/ S)) - ( Sum S))

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, S,T be finite Subset of V;

      (T \ S) misses S by XBOOLE_1: 79;

      then

       A1: ((T \ S) /\ S) = ( {} V);

      ((T \ S) \/ S) = (T \/ S) by XBOOLE_1: 39;

      then ( Sum (T \/ S)) = ((( Sum (T \ S)) + ( Sum S)) - ( Sum ((T \ S) /\ S))) by Th13;

      

      then ( Sum (T \/ S)) = ((( Sum (T \ S)) + ( Sum S)) - ( 0. V)) by A1, Th8

      .= (( Sum (T \ S)) + ( Sum S));

      hence thesis by RLSUB_2: 61;

    end;

    theorem :: RLVECT_2:16

    

     Th16: for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, S,T be finite Subset of V holds ( Sum (T \ S)) = (( Sum T) - ( Sum (T /\ S)))

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, S,T be finite Subset of V;

      (T \ (T /\ S)) = (T \ S) by XBOOLE_1: 47;

      then ( Sum (T \ S)) = (( Sum (T \/ (T /\ S))) - ( Sum (T /\ S))) by Th15;

      hence thesis by XBOOLE_1: 22;

    end;

    theorem :: RLVECT_2:17

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, S,T be finite Subset of V holds ( Sum (T \+\ S)) = (( Sum (T \/ S)) - ( Sum (T /\ S)))

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, S,T be finite Subset of V;

      (T \+\ S) = ((T \/ S) \ (T /\ S)) by XBOOLE_1: 101;

      

      hence ( Sum (T \+\ S)) = (( Sum (T \/ S)) - ( Sum ((T \/ S) /\ (T /\ S)))) by Th16

      .= (( Sum (T \/ S)) - ( Sum (((T \/ S) /\ T) /\ S))) by XBOOLE_1: 16

      .= (( Sum (T \/ S)) - ( Sum (T /\ S))) by XBOOLE_1: 21;

    end;

    theorem :: RLVECT_2:18

    for V be Abelian add-associative right_zeroed non empty addLoopStr, S,T be finite Subset of V holds ( Sum (T \+\ S)) = (( Sum (T \ S)) + ( Sum (S \ T))) by Th12, XBOOLE_1: 82;

    reconsider zz = 0 as Element of REAL by XREAL_0:def 1;

    definition

      let V be non empty ZeroStr;

      :: RLVECT_2:def3

      mode Linear_Combination of V -> Element of ( Funcs (the carrier of V, REAL )) means

      : Def3: ex T be finite Subset of V st for v be Element of V st not v in T holds (it . v) = 0 ;

      existence

      proof

        reconsider f = (the carrier of V --> zz) as Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

        take f, ( {} V);

        thus thesis by FUNCOP_1: 7;

      end;

    end

    reserve K,L,L1,L2,L3 for Linear_Combination of V;

    notation

      let V be non empty addLoopStr, L be Element of ( Funcs (the carrier of V, REAL ));

      synonym Carrier L for support L;

    end

     Lm1:

    now

      let V be non empty addLoopStr, L be Element of ( Funcs (the carrier of V, REAL ));

      

       A1: ( support L) c= ( dom L) by PRE_POLY: 37;

      thus ( Carrier L) c= the carrier of V

      proof

        let x be object;

        assume x in ( support L);

        then x in ( dom L) by A1;

        hence thesis;

      end;

    end;

    definition

      let V be non empty addLoopStr, L be Element of ( Funcs (the carrier of V, REAL ));

      :: original: Carrier

      redefine

      :: RLVECT_2:def4

      func Carrier (L) -> Subset of V equals { v where v be Element of V : (L . v) <> 0 };

      coherence by Lm1;

      compatibility

      proof

        let X be Subset of V;

        set A = ( Carrier L);

        set B = { v where v be Element of V : (L . v) <> 0 };

        thus X = A implies X = B

        proof

          assume

           A1: X = A;

          thus X c= B

          proof

            let x be object;

            assume

             A2: x in X;

            then (L . x) <> 0 by A1, PRE_POLY:def 7;

            hence thesis by A2;

          end;

          let x be object;

          assume x in B;

          then ex v be Element of V st x = v & (L . v) <> 0 ;

          hence thesis by A1, PRE_POLY:def 7;

        end;

        assume

         A3: X = B;

        thus X c= A

        proof

          let x be object;

          assume x in X;

          then ex v be Element of V st x = v & (L . v) <> 0 by A3;

          hence thesis by PRE_POLY:def 7;

        end;

        let x be object;

        assume

         A4: x in A;

        then

         A5: (L . x) <> 0 by PRE_POLY:def 7;

        ( Carrier L) c= the carrier of V by Lm1;

        hence thesis by A3, A4, A5;

      end;

    end

    registration

      let V be non empty addLoopStr, L be Linear_Combination of V;

      cluster ( Carrier L) -> finite;

      coherence

      proof

        set A = ( Carrier L);

        consider T be finite Subset of V such that

         A1: for v be Element of V st not v in T holds (L . v) = 0 by Def3;

        A c= T

        proof

          let x be object;

          assume x in A;

          then ex v be Element of V st x = v & (L . v) <> 0 ;

          hence thesis by A1;

        end;

        hence thesis;

      end;

    end

    theorem :: RLVECT_2:19

    for V be non empty addLoopStr, L be Linear_Combination of V, v be Element of V holds (L . v) = 0 iff not v in ( Carrier L)

    proof

      let V be non empty addLoopStr, L be Linear_Combination of V, v be Element of V;

      thus (L . v) = 0 implies not v in ( Carrier L)

      proof

        assume

         A1: (L . v) = 0 ;

        assume not thesis;

        then ex u be Element of V st u = v & (L . u) <> 0 ;

        hence thesis by A1;

      end;

      thus thesis;

    end;

    definition

      let V be non empty addLoopStr;

      :: RLVECT_2:def5

      func ZeroLC (V) -> Linear_Combination of V means

      : Def5: ( Carrier it ) = {} ;

      existence

      proof

        reconsider f = (the carrier of V --> zz) as Function of the carrier of V, REAL ;

        reconsider f as Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

        f is Linear_Combination of V

        proof

          reconsider T = ( {} V) as empty finite Subset of V;

          take T;

          thus thesis by FUNCOP_1: 7;

        end;

        then

        reconsider f as Linear_Combination of V;

        take f;

        set C = { v where v be Element of V : (f . v) <> 0 };

        now

          set x = the Element of C;

          assume C <> {} ;

          then x in C;

          then ex v be Element of V st x = v & (f . v) <> 0 ;

          hence contradiction by FUNCOP_1: 7;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let L,L9 be Linear_Combination of V;

        assume that

         A1: ( Carrier L) = {} and

         A2: ( Carrier L9) = {} ;

        now

          let x be object;

          assume x in the carrier of V;

          then

          reconsider v = x as Element of V;

           A3:

          now

            assume (L9 . v) <> 0 ;

            then v in { u where u be Element of V : (L9 . u) <> 0 };

            hence contradiction by A2;

          end;

          now

            assume (L . v) <> 0 ;

            then v in { u where u be Element of V : (L . u) <> 0 };

            hence contradiction by A1;

          end;

          hence (L . x) = (L9 . x) by A3;

        end;

        hence L = L9;

      end;

    end

    theorem :: RLVECT_2:20

    

     Th20: for V be non empty addLoopStr, v be Element of V holds (( ZeroLC V) . v) = 0

    proof

      let V be non empty addLoopStr, v be Element of V;

      ( Carrier ( ZeroLC V)) = {} & not v in {} by Def5;

      hence thesis;

    end;

    definition

      let V be non empty addLoopStr;

      let A be Subset of V;

      :: RLVECT_2:def6

      mode Linear_Combination of A -> Linear_Combination of V means

      : Def6: ( Carrier it ) c= A;

      existence

      proof

        take L = ( ZeroLC V);

        ( Carrier L) = {} by Def5;

        hence thesis;

      end;

    end

    reserve l,l1,l2 for Linear_Combination of A;

    theorem :: RLVECT_2:21

    A c= B implies l is Linear_Combination of B

    proof

      assume

       A1: A c= B;

      ( Carrier l) c= A by Def6;

      then ( Carrier l) c= B by A1;

      hence thesis by Def6;

    end;

    theorem :: RLVECT_2:22

    

     Th22: ( ZeroLC V) is Linear_Combination of A

    proof

      ( Carrier ( ZeroLC V)) = {} & {} c= A by Def5;

      hence thesis by Def6;

    end;

    theorem :: RLVECT_2:23

    

     Th23: for l be Linear_Combination of ( {} the carrier of V) holds l = ( ZeroLC V)

    proof

      let l be Linear_Combination of ( {} the carrier of V);

      ( Carrier l) c= {} by Def6;

      then ( Carrier l) = {} ;

      hence thesis by Def5;

    end;

    definition

      let V;

      let F;

      let f;

      :: RLVECT_2:def7

      func f (#) F -> FinSequence of the carrier of V means

      : Def7: ( len it ) = ( len F) & for i st i in ( dom it ) holds (it . i) = ((f . (F /. i)) * (F /. i));

      existence

      proof

        deffunc Q( set) = ((f . (F /. $1)) * (F /. $1));

        consider G be FinSequence such that

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

         A2: for n be Nat st n in ( dom G) holds (G . n) = Q(n) from FINSEQ_1:sch 2;

        ( rng G) c= the carrier of V

        proof

          let x be object;

          assume x in ( rng G);

          then

          consider y be object such that

           A3: y in ( dom G) and

           A4: (G . y) = x by FUNCT_1:def 3;

          y in ( Seg ( len F)) by A1, A3, FINSEQ_1:def 3;

          then

          reconsider y as Element of NAT ;

          (G . y) = ((f . (F /. y)) * (F /. y)) by A2, A3;

          hence thesis by A4;

        end;

        then

        reconsider G as FinSequence of the carrier of V by FINSEQ_1:def 4;

        take G;

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let H1, H2;

        assume that

         A5: ( len H1) = ( len F) and

         A6: for i st i in ( dom H1) holds (H1 . i) = ((f . (F /. i)) * (F /. i)) and

         A7: ( len H2) = ( len F) and

         A8: for i st i in ( dom H2) holds (H2 . i) = ((f . (F /. i)) * (F /. i));

        now

          let k be Nat;

          assume 1 <= k & k <= ( len H1);

          then

           A9: k in ( Seg ( len H1)) by FINSEQ_1: 1;

          then k in ( dom H1) by FINSEQ_1:def 3;

          then

           A10: (H1 . k) = ((f . (F /. k)) * (F /. k)) by A6;

          k in ( dom H2) by A5, A7, A9, FINSEQ_1:def 3;

          hence (H1 . k) = (H2 . k) by A8, A10;

        end;

        hence thesis by A5, A7, FINSEQ_1: 14;

      end;

    end

    theorem :: RLVECT_2:24

    

     Th24: i in ( dom F) & v = (F . i) implies ((f (#) F) . i) = ((f . v) * v)

    proof

      assume that

       A1: i in ( dom F) and

       A2: v = (F . i);

      

       A3: (F /. i) = (F . i) by A1, PARTFUN1:def 6;

      ( len (f (#) F)) = ( len F) by Def7;

      then i in ( dom (f (#) F)) by A1, FINSEQ_3: 29;

      hence thesis by A2, A3, Def7;

    end;

    theorem :: RLVECT_2:25

    (f (#) ( <*> the carrier of V)) = ( <*> the carrier of V)

    proof

      ( len (f (#) ( <*> the carrier of V))) = ( len ( <*> the carrier of V)) by Def7

      .= 0 ;

      hence thesis;

    end;

    theorem :: RLVECT_2:26

    

     Th26: (f (#) <*v*>) = <*((f . v) * v)*>

    proof

      

       A1: 1 in {1} by TARSKI:def 1;

      

       A2: ( len (f (#) <*v*>)) = ( len <*v*>) by Def7

      .= 1 by FINSEQ_1: 40;

      then ( dom (f (#) <*v*>)) = {1} by FINSEQ_1: 2, FINSEQ_1:def 3;

      

      then ((f (#) <*v*>) . 1) = ((f . ( <*v*> /. 1)) * ( <*v*> /. 1)) by A1, Def7

      .= ((f . ( <*v*> /. 1)) * v) by FINSEQ_4: 16

      .= ((f . v) * v) by FINSEQ_4: 16;

      hence thesis by A2, FINSEQ_1: 40;

    end;

    theorem :: RLVECT_2:27

    

     Th27: (f (#) <*v1, v2*>) = <*((f . v1) * v1), ((f . v2) * v2)*>

    proof

      

       A1: ( len (f (#) <*v1, v2*>)) = ( len <*v1, v2*>) by Def7

      .= 2 by FINSEQ_1: 44;

      then

       A2: ( dom (f (#) <*v1, v2*>)) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

      2 in {1, 2} by TARSKI:def 2;

      

      then

       A3: ((f (#) <*v1, v2*>) . 2) = ((f . ( <*v1, v2*> /. 2)) * ( <*v1, v2*> /. 2)) by A2, Def7

      .= ((f . ( <*v1, v2*> /. 2)) * v2) by FINSEQ_4: 17

      .= ((f . v2) * v2) by FINSEQ_4: 17;

      1 in {1, 2} by TARSKI:def 2;

      

      then ((f (#) <*v1, v2*>) . 1) = ((f . ( <*v1, v2*> /. 1)) * ( <*v1, v2*> /. 1)) by A2, Def7

      .= ((f . ( <*v1, v2*> /. 1)) * v1) by FINSEQ_4: 17

      .= ((f . v1) * v1) by FINSEQ_4: 17;

      hence thesis by A1, A3, FINSEQ_1: 44;

    end;

    theorem :: RLVECT_2:28

    (f (#) <*v1, v2, v3*>) = <*((f . v1) * v1), ((f . v2) * v2), ((f . v3) * v3)*>

    proof

      

       A1: ( len (f (#) <*v1, v2, v3*>)) = ( len <*v1, v2, v3*>) by Def7

      .= 3 by FINSEQ_1: 45;

      then

       A2: ( dom (f (#) <*v1, v2, v3*>)) = {1, 2, 3} by FINSEQ_1:def 3, FINSEQ_3: 1;

      3 in {1, 2, 3} by ENUMSET1:def 1;

      

      then

       A3: ((f (#) <*v1, v2, v3*>) . 3) = ((f . ( <*v1, v2, v3*> /. 3)) * ( <*v1, v2, v3*> /. 3)) by A2, Def7

      .= ((f . ( <*v1, v2, v3*> /. 3)) * v3) by FINSEQ_4: 18

      .= ((f . v3) * v3) by FINSEQ_4: 18;

      2 in {1, 2, 3} by ENUMSET1:def 1;

      

      then

       A4: ((f (#) <*v1, v2, v3*>) . 2) = ((f . ( <*v1, v2, v3*> /. 2)) * ( <*v1, v2, v3*> /. 2)) by A2, Def7

      .= ((f . ( <*v1, v2, v3*> /. 2)) * v2) by FINSEQ_4: 18

      .= ((f . v2) * v2) by FINSEQ_4: 18;

      1 in {1, 2, 3} by ENUMSET1:def 1;

      

      then ((f (#) <*v1, v2, v3*>) . 1) = ((f . ( <*v1, v2, v3*> /. 1)) * ( <*v1, v2, v3*> /. 1)) by A2, Def7

      .= ((f . ( <*v1, v2, v3*> /. 1)) * v1) by FINSEQ_4: 18

      .= ((f . v1) * v1) by FINSEQ_4: 18;

      hence thesis by A1, A4, A3, FINSEQ_1: 45;

    end;

    definition

      let V;

      let L;

      :: RLVECT_2:def8

      func Sum (L) -> Element of V means

      : Def8: ex F st F is one-to-one & ( rng F) = ( Carrier L) & it = ( Sum (L (#) F));

      existence

      proof

        consider F be FinSequence such that

         A1: ( rng F) = ( Carrier L) and

         A2: F is one-to-one by FINSEQ_4: 58;

        reconsider F as FinSequence of the carrier of V by A1, FINSEQ_1:def 4;

        take ( Sum (L (#) F));

        take F;

        thus F is one-to-one & ( rng F) = ( Carrier L) by A1, A2;

        thus thesis;

      end;

      uniqueness

      proof

        let v1,v2 be Element of V;

        given F1 be FinSequence of the carrier of V such that

         A3: F1 is one-to-one and

         A4: ( rng F1) = ( Carrier L) and

         A5: v1 = ( Sum (L (#) F1));

        given F2 be FinSequence of the carrier of V such that

         A6: F2 is one-to-one and

         A7: ( rng F2) = ( Carrier L) and

         A8: v2 = ( Sum (L (#) F2));

        defpred P[ object, object] means {$2} = (F1 " {(F2 . $1)});

        

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

        

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

        

         A11: ( len F1) = ( len F2) by A3, A4, A6, A7, FINSEQ_1: 48;

        

         A12: for x be object st x in ( dom F1) holds ex y be object st y in ( dom F1) & P[x, y]

        proof

          let x be object;

          assume x in ( dom F1);

          then (F2 . x) in ( rng F1) by A4, A7, A11, A10, A9, FUNCT_1:def 3;

          then

          consider y be object such that

           A13: (F1 " {(F2 . x)}) = {y} by A3, FUNCT_1: 74;

          take y;

          y in (F1 " {(F2 . x)}) by A13, TARSKI:def 1;

          hence y in ( dom F1) by FUNCT_1:def 7;

          thus thesis by A13;

        end;

        consider f be Function of ( dom F1), ( dom F1) such that

         A14: for x be object st x in ( dom F1) holds P[x, (f . x)] from FUNCT_2:sch 1( A12);

        

         A15: f is one-to-one

        proof

          let y1,y2 be object;

          assume that

           A16: y1 in ( dom f) and

           A17: y2 in ( dom f) and

           A18: (f . y1) = (f . y2);

          (F2 . y1) in ( rng F1) by A4, A7, A11, A10, A9, A16, FUNCT_1:def 3;

          then

           A19: {(F2 . y1)} c= ( rng F1) by ZFMISC_1: 31;

          (F2 . y2) in ( rng F1) by A4, A7, A11, A10, A9, A17, FUNCT_1:def 3;

          then

           A20: {(F2 . y2)} c= ( rng F1) by ZFMISC_1: 31;

          (F1 " {(F2 . y1)}) = {(f . y1)} & (F1 " {(F2 . y2)}) = {(f . y2)} by A14, A16, A17;

          then {(F2 . y1)} = {(F2 . y2)} by A18, A19, A20, FUNCT_1: 91;

          then (F2 . y1) = (F2 . y2) by ZFMISC_1: 3;

          hence thesis by A6, A11, A10, A9, A16, A17;

        end;

        set G1 = (L (#) F1);

        

         A21: ( len G1) = ( len F1) by Def7;

        

         A22: ( rng f) = ( dom F1)

        proof

          thus ( rng f) c= ( dom F1);

          let y be object;

          assume

           A23: y in ( dom F1);

          then (F1 . y) in ( rng F2) by A4, A7, FUNCT_1:def 3;

          then

          consider x be object such that

           A24: x in ( dom F2) and

           A25: (F2 . x) = (F1 . y) by FUNCT_1:def 3;

          (F1 " {(F2 . x)}) = (F1 " ( Im (F1,y))) by A23, A25, FUNCT_1: 59;

          then (F1 " {(F2 . x)}) c= {y} by A3, FUNCT_1: 82;

          then {(f . x)} c= {y} by A11, A10, A9, A14, A24;

          then

           A26: (f . x) = y by ZFMISC_1: 18;

          x in ( dom f) by A11, A10, A9, A24, FUNCT_2:def 1;

          hence thesis by A26, FUNCT_1:def 3;

        end;

        then

        reconsider f as Permutation of ( dom F1) by A15, FUNCT_2: 57;

        ( dom F1) = ( Seg ( len F1)) & ( dom G1) = ( Seg ( len G1)) by FINSEQ_1:def 3;

        then

        reconsider f as Permutation of ( dom G1) by A21;

        set G2 = (L (#) F2);

        

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

        

         A28: ( len G2) = ( len F2) by Def7;

        

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

        now

          let i;

          assume

           A30: i in ( dom G2);

          then

          reconsider u = (F2 . i) as VECTOR of V by A28, A9, A27, FUNCT_1: 102;

          

           A31: (G2 . i) = ((L . (F2 /. i)) * (F2 /. i)) & (F2 . i) = (F2 /. i) by A28, A9, A27, A30, Def7, PARTFUN1:def 6;

          i in ( dom f) by A11, A21, A28, A29, A27, A30, FUNCT_2:def 1;

          then

           A32: (f . i) in ( dom F1) by A22, FUNCT_1:def 3;

          then

          reconsider m = (f . i) as Element of NAT ;

          reconsider v = (F1 . m) as VECTOR of V by A32, FUNCT_1: 102;

           {(F1 . (f . i))} = ( Im (F1,(f . i))) by A32, FUNCT_1: 59

          .= (F1 .: (F1 " {(F2 . i)})) by A11, A28, A10, A27, A14, A30;

          then

           A33: u = v by FUNCT_1: 75, ZFMISC_1: 18;

          (F1 . m) = (F1 /. m) by A32, PARTFUN1:def 6;

          hence (G2 . i) = (G1 . (f . i)) by A21, A10, A29, A32, A33, A31, Def7;

        end;

        hence thesis by A3, A4, A5, A6, A7, A8, A21, A28, Th6, FINSEQ_1: 48;

      end;

    end

    

     Lm2: ( Sum ( ZeroLC V)) = ( 0. V)

    proof

      consider F such that F is one-to-one and

       A1: ( rng F) = ( Carrier ( ZeroLC V)) and

       A2: ( Sum ( ZeroLC V)) = ( Sum (( ZeroLC V) (#) F)) by Def8;

      ( Carrier ( ZeroLC V)) = {} by Def5;

      then F = {} by A1, RELAT_1: 41;

      then ( len F) = 0 ;

      then ( len (( ZeroLC V) (#) F)) = 0 by Def7;

      hence thesis by A2, RLVECT_1: 75;

    end;

    theorem :: RLVECT_2:29

    A <> {} & A is linearly-closed iff for l holds ( Sum l) in A

    proof

      thus A <> {} & A is linearly-closed implies for l holds ( Sum l) in A

      proof

        defpred P[ Nat] means for l st ( card ( Carrier l)) = $1 holds ( Sum l) in A;

        assume that

         A1: A <> {} and

         A2: A is linearly-closed;

        now

          let l;

          assume ( card ( Carrier l)) = 0 ;

          then ( Carrier l) = {} ;

          then l = ( ZeroLC V) by Def5;

          then ( Sum l) = ( 0. V) by Lm2;

          hence ( Sum l) in A by A1, A2, RLSUB_1: 1;

        end;

        then

         A3: P[ 0 ];

        now

          let k;

          assume

           A4: for l st ( card ( Carrier l)) = k holds ( Sum l) in A;

          let l;

          deffunc F( Element of V) = (l . $1);

          consider F such that

           A5: F is one-to-one and

           A6: ( rng F) = ( Carrier l) and

           A7: ( Sum l) = ( Sum (l (#) F)) by Def8;

          reconsider G = (F | ( Seg k)) as FinSequence of the carrier of V by FINSEQ_1: 18;

          assume

           A8: ( card ( Carrier l)) = (k + 1);

          then

           A9: ( len F) = (k + 1) by A5, A6, FINSEQ_4: 62;

          then

           A10: ( len (l (#) F)) = (k + 1) by Def7;

          

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

          then

           A12: (k + 1) in ( dom F) by A9, FINSEQ_1:def 3;

          (k + 1) in ( dom F) by A9, A11, FINSEQ_1:def 3;

          then

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

          consider f be Function of the carrier of V, REAL such that

           A13: (f . v) = ( In ( 0 , REAL )) and

           A14: for u be Element of V st u <> v holds (f . u) = F(u) from FUNCT_2:sch 6;

          reconsider f as Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

          

           A15: v in ( Carrier l) by A6, A12, FUNCT_1:def 3;

          now

            let u;

            assume

             A16: not u in ( Carrier l);

            

            hence (f . u) = (l . u) by A15, A14

            .= 0 by A16;

          end;

          then

          reconsider f as Linear_Combination of V by Def3;

          

           A17: (A \ {v}) c= A by XBOOLE_1: 36;

          

           A18: ( Carrier l) c= A by Def6;

          then

           A19: ((l . v) * v) in A by A2, A15;

          

           A20: ( Carrier f) = (( Carrier l) \ {v})

          proof

            thus ( Carrier f) c= (( Carrier l) \ {v})

            proof

              let x be object;

              assume x in ( Carrier f);

              then

              consider u such that

               A21: u = x and

               A22: (f . u) <> 0 ;

              (f . u) = (l . u) by A13, A14, A22;

              then

               A23: x in ( Carrier l) by A21, A22;

               not x in {v} by A13, A21, A22, TARSKI:def 1;

              hence thesis by A23, XBOOLE_0:def 5;

            end;

            let x be object;

            assume

             A24: x in (( Carrier l) \ {v});

            then x in ( Carrier l) by XBOOLE_0:def 5;

            then

            consider u such that

             A25: x = u and

             A26: (l . u) <> 0 ;

             not x in {v} by A24, XBOOLE_0:def 5;

            then x <> v by TARSKI:def 1;

            then (l . u) = (f . u) by A14, A25;

            hence thesis by A25, A26;

          end;

          then ( Carrier f) c= (A \ {v}) by A18, XBOOLE_1: 33;

          then ( Carrier f) c= A by A17;

          then

          reconsider f as Linear_Combination of A by Def6;

          

           A27: ( len G) = k by A9, FINSEQ_3: 53;

          then

           A28: ( len (f (#) G)) = k by Def7;

          

           A29: ( rng G) = ( Carrier f)

          proof

            thus ( rng G) c= ( Carrier f)

            proof

              let x be object;

              assume x in ( rng G);

              then

              consider y be object such that

               A30: y in ( dom G) and

               A31: (G . y) = x by FUNCT_1:def 3;

              reconsider y as Element of NAT by A30;

              

               A32: ( dom G) c= ( dom F) & (G . y) = (F . y) by A30, FUNCT_1: 47, RELAT_1: 60;

              now

                assume x = v;

                then

                 A33: (k + 1) = y by A5, A12, A30, A31, A32;

                y <= k by A27, A30, FINSEQ_3: 25;

                hence contradiction by A33, XREAL_1: 29;

              end;

              then

               A34: not x in {v} by TARSKI:def 1;

              x in ( rng F) by A30, A31, A32, FUNCT_1:def 3;

              hence thesis by A6, A20, A34, XBOOLE_0:def 5;

            end;

            let x be object;

            assume

             A35: x in ( Carrier f);

            then x in ( rng F) by A6, A20, XBOOLE_0:def 5;

            then

            consider y be object such that

             A36: y in ( dom F) and

             A37: (F . y) = x by FUNCT_1:def 3;

            reconsider y as Element of NAT by A36;

            now

              assume not y in ( Seg k);

              then y in (( dom F) \ ( Seg k)) by A36, XBOOLE_0:def 5;

              then y in (( Seg (k + 1)) \ ( Seg k)) by A9, FINSEQ_1:def 3;

              then y in {(k + 1)} by FINSEQ_3: 15;

              then y = (k + 1) by TARSKI:def 1;

              then not v in {v} by A20, A35, A37, XBOOLE_0:def 5;

              hence contradiction by TARSKI:def 1;

            end;

            then y in (( dom F) /\ ( Seg k)) by A36, XBOOLE_0:def 4;

            then

             A38: y in ( dom G) by RELAT_1: 61;

            then (G . y) = (F . y) by FUNCT_1: 47;

            hence thesis by A37, A38, FUNCT_1:def 3;

          end;

          (( Seg (k + 1)) /\ ( Seg k)) = ( Seg k) by FINSEQ_1: 7, NAT_1: 12

          .= ( dom (f (#) G)) by A28, FINSEQ_1:def 3;

          then

           A39: ( dom (f (#) G)) = (( dom (l (#) F)) /\ ( Seg k)) by A10, FINSEQ_1:def 3;

          now

            let x be object;

            assume

             A40: x in ( dom (f (#) G));

            then

            reconsider n = x as Element of NAT ;

            n in ( dom (l (#) F)) by A39, A40, XBOOLE_0:def 4;

            then

             A41: n in ( dom F) by A9, A10, FINSEQ_3: 29;

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

            then

            reconsider w = (F . n) as VECTOR of V;

            

             A42: n in ( dom G) by A27, A28, A40, FINSEQ_3: 29;

            then

             A43: (G . n) in ( rng G) by FUNCT_1:def 3;

            then

            reconsider u = (G . n) as VECTOR of V;

             not u in {v} by A20, A29, A43, XBOOLE_0:def 5;

            then

             A44: u <> v by TARSKI:def 1;

            

             A45: ((f (#) G) . n) = ((f . u) * u) by A42, Th24

            .= ((l . u) * u) by A14, A44;

            w = u by A42, FUNCT_1: 47;

            hence ((f (#) G) . x) = ((l (#) F) . x) by A45, A41, Th24;

          end;

          then

           A46: (f (#) G) = ((l (#) F) | ( Seg k)) by A39, FUNCT_1: 46;

          v in ( rng F) by A12, FUNCT_1:def 3;

          then {v} c= ( Carrier l) by A6, ZFMISC_1: 31;

          

          then ( card ( Carrier f)) = ((k + 1) - ( card {v})) by A8, A20, CARD_2: 44

          .= ((k + 1) - 1) by CARD_1: 30

          .= k;

          then

           A47: ( Sum f) in A by A4;

          G is one-to-one by A5, FUNCT_1: 52;

          then

           A48: ( Sum (f (#) G)) = ( Sum f) by A29, Def8;

          ( dom (f (#) G)) = ( Seg ( len (f (#) G))) & ((l (#) F) . ( len F)) = ((l . v) * v) by A9, A12, Th24, FINSEQ_1:def 3;

          then ( Sum (l (#) F)) = (( Sum (f (#) G)) + ((l . v) * v)) by A9, A10, A28, A46, RLVECT_1: 38;

          hence ( Sum l) in A by A2, A7, A19, A48, A47;

        end;

        then

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

        let l;

        

         A50: ( card ( Carrier l)) = ( card ( Carrier l));

        for k holds P[k] from NAT_1:sch 2( A3, A49);

        hence thesis by A50;

      end;

      assume

       A51: for l holds ( Sum l) in A;

      hence A <> {} ;

      ( ZeroLC V) is Linear_Combination of A & ( Sum ( ZeroLC V)) = ( 0. V) by Lm2, Th22;

      then

       A52: ( 0. V) in A by A51;

      

       A53: for a, v st v in A holds (a * v) in A

      proof

        let a, v;

        assume

         A54: v in A;

        now

          per cases ;

            suppose a = 0 ;

            hence thesis by A52, RLVECT_1: 10;

          end;

            suppose

             A55: a <> 0 ;

            deffunc F( Element of V) = zz;

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

            consider f such that

             A56: (f . v) = aa and

             A57: for u be Element of V st u <> v holds (f . u) = F(u) from FUNCT_2:sch 6;

            reconsider f as Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

            now

              let u;

              assume not u in {v};

              then u <> v by TARSKI:def 1;

              hence (f . u) = 0 by A57;

            end;

            then

            reconsider f as Linear_Combination of V by Def3;

            

             A58: ( Carrier f) = {v}

            proof

              thus ( Carrier f) c= {v}

              proof

                let x be object;

                assume x in ( Carrier f);

                then

                consider u such that

                 A59: x = u and

                 A60: (f . u) <> 0 ;

                u = v by A57, A60;

                hence thesis by A59, TARSKI:def 1;

              end;

              let x be object;

              assume x in {v};

              then x = v by TARSKI:def 1;

              hence thesis by A55, A56;

            end;

             {v} c= A by A54, ZFMISC_1: 31;

            then

            reconsider f as Linear_Combination of A by A58, Def6;

            consider F such that

             A61: F is one-to-one & ( rng F) = ( Carrier f) and

             A62: ( Sum (f (#) F)) = ( Sum f) by Def8;

            F = <*v*> by A58, A61, FINSEQ_3: 97;

            then (f (#) F) = <*((f . v) * v)*> by Th26;

            then ( Sum f) = (a * v) by A56, A62, RLVECT_1: 44;

            hence thesis by A51;

          end;

        end;

        hence thesis;

      end;

      thus for v, u st v in A & u in A holds (v + u) in A

      proof

        let v, u;

        assume that

         A63: v in A and

         A64: u in A;

        now

          per cases ;

            suppose u = v;

            

            then (v + u) = ((1 * v) + v) by RLVECT_1:def 8

            .= ((1 * v) + (1 * v)) by RLVECT_1:def 8

            .= ((1 + 1) * v) by RLVECT_1:def 6

            .= (2 * v);

            hence thesis by A53, A63;

          end;

            suppose

             A65: v <> u;

            deffunc F( Element of V) = zz;

            reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

            consider f such that

             A66: (f . v) = jj & (f . u) = jj and

             A67: for w be Element of V st w <> v & w <> u holds (f . w) = F(w) from FUNCT_2:sch 7( A65);

            reconsider f as Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

            now

              let w;

              assume not w in {v, u};

              then w <> v & w <> u by TARSKI:def 2;

              hence (f . w) = 0 by A67;

            end;

            then

            reconsider f as Linear_Combination of V by Def3;

            

             A68: ( Carrier f) = {v, u}

            proof

              thus ( Carrier f) c= {v, u}

              proof

                let x be object;

                assume x in ( Carrier f);

                then ex w st x = w & (f . w) <> 0 ;

                then x = v or x = u by A67;

                hence thesis by TARSKI:def 2;

              end;

              let x be object;

              assume x in {v, u};

              then x = v or x = u by TARSKI:def 2;

              hence thesis by A66;

            end;

            then

             A69: ( Carrier f) c= A by A63, A64, ZFMISC_1: 32;

            

             A70: (1 * u) = u & (1 * v) = v by RLVECT_1:def 8;

            reconsider f as Linear_Combination of A by A69, Def6;

            consider F such that

             A71: F is one-to-one & ( rng F) = ( Carrier f) and

             A72: ( Sum (f (#) F)) = ( Sum f) by Def8;

            F = <*v, u*> or F = <*u, v*> by A65, A68, A71, FINSEQ_3: 99;

            then (f (#) F) = <*(1 * v), (1 * u)*> or (f (#) F) = <*(1 * u), (1 * v)*> by A66, Th27;

            then ( Sum f) = (v + u) by A72, A70, RLVECT_1: 45;

            hence thesis by A51;

          end;

        end;

        hence thesis;

      end;

      thus thesis by A53;

    end;

    theorem :: RLVECT_2:30

    ( Sum ( ZeroLC V)) = ( 0. V) by Lm2;

    theorem :: RLVECT_2:31

    for l be Linear_Combination of ( {} the carrier of V) holds ( Sum l) = ( 0. V)

    proof

      let l be Linear_Combination of ( {} the carrier of V);

      l = ( ZeroLC V) by Th23;

      hence thesis by Lm2;

    end;

    theorem :: RLVECT_2:32

    

     Th32: for l be Linear_Combination of {v} holds ( Sum l) = ((l . v) * v)

    proof

      let l be Linear_Combination of {v};

      

       A1: ( Carrier l) c= {v} by Def6;

      now

        per cases by A1, ZFMISC_1: 33;

          suppose ( Carrier l) = {} ;

          then

           A2: l = ( ZeroLC V) by Def5;

          

          hence ( Sum l) = ( 0. V) by Lm2

          .= ( 0 * v) by RLVECT_1: 10

          .= ((l . v) * v) by A2, Th20;

        end;

          suppose ( Carrier l) = {v};

          then

          consider F such that

           A3: F is one-to-one & ( rng F) = {v} and

           A4: ( Sum l) = ( Sum (l (#) F)) by Def8;

          F = <*v*> by A3, FINSEQ_3: 97;

          then (l (#) F) = <*((l . v) * v)*> by Th26;

          hence thesis by A4, RLVECT_1: 44;

        end;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_2:33

    

     Th33: v1 <> v2 implies for l be Linear_Combination of {v1, v2} holds ( Sum l) = (((l . v1) * v1) + ((l . v2) * v2))

    proof

      assume

       A1: v1 <> v2;

      let l be Linear_Combination of {v1, v2};

      

       A2: ( Carrier l) c= {v1, v2} by Def6;

      now

        per cases by A2, ZFMISC_1: 36;

          suppose ( Carrier l) = {} ;

          then

           A3: l = ( ZeroLC V) by Def5;

          

          hence ( Sum l) = ( 0. V) by Lm2

          .= (( 0. V) + ( 0. V))

          .= (( 0 * v1) + ( 0. V)) by RLVECT_1: 10

          .= (( 0 * v1) + ( 0 * v2)) by RLVECT_1: 10

          .= (((l . v1) * v1) + ( 0 * v2)) by A3, Th20

          .= (((l . v1) * v1) + ((l . v2) * v2)) by A3, Th20;

        end;

          suppose

           A4: ( Carrier l) = {v1};

          then

          reconsider L = l as Linear_Combination of {v1} by Def6;

          

           A5: not v2 in ( Carrier l) by A1, A4, TARSKI:def 1;

          

          thus ( Sum l) = ( Sum L)

          .= ((l . v1) * v1) by Th32

          .= (((l . v1) * v1) + ( 0. V))

          .= (((l . v1) * v1) + ( 0 * v2)) by RLVECT_1: 10

          .= (((l . v1) * v1) + ((l . v2) * v2)) by A5;

        end;

          suppose

           A6: ( Carrier l) = {v2};

          then

          reconsider L = l as Linear_Combination of {v2} by Def6;

          

           A7: not v1 in ( Carrier l) by A1, A6, TARSKI:def 1;

          

          thus ( Sum l) = ( Sum L)

          .= ((l . v2) * v2) by Th32

          .= (( 0. V) + ((l . v2) * v2))

          .= (( 0 * v1) + ((l . v2) * v2)) by RLVECT_1: 10

          .= (((l . v1) * v1) + ((l . v2) * v2)) by A7;

        end;

          suppose ( Carrier l) = {v1, v2};

          then

          consider F such that

           A8: F is one-to-one & ( rng F) = {v1, v2} and

           A9: ( Sum l) = ( Sum (l (#) F)) by Def8;

          F = <*v1, v2*> or F = <*v2, v1*> by A1, A8, FINSEQ_3: 99;

          then (l (#) F) = <*((l . v1) * v1), ((l . v2) * v2)*> or (l (#) F) = <*((l . v2) * v2), ((l . v1) * v1)*> by Th27;

          hence thesis by A9, RLVECT_1: 45;

        end;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_2:34

    ( Carrier L) = {} implies ( Sum L) = ( 0. V)

    proof

      assume ( Carrier L) = {} ;

      then L = ( ZeroLC V) by Def5;

      hence thesis by Lm2;

    end;

    theorem :: RLVECT_2:35

    ( Carrier L) = {v} implies ( Sum L) = ((L . v) * v)

    proof

      assume ( Carrier L) = {v};

      then L is Linear_Combination of {v} by Def6;

      hence thesis by Th32;

    end;

    theorem :: RLVECT_2:36

    ( Carrier L) = {v1, v2} & v1 <> v2 implies ( Sum L) = (((L . v1) * v1) + ((L . v2) * v2))

    proof

      assume that

       A1: ( Carrier L) = {v1, v2} and

       A2: v1 <> v2;

      L is Linear_Combination of {v1, v2} by A1, Def6;

      hence thesis by A2, Th33;

    end;

    definition

      let V be non empty addLoopStr;

      let L1,L2 be Linear_Combination of V;

      :: original: =

      redefine

      :: RLVECT_2:def9

      pred L1 = L2 means for v be Element of V holds (L1 . v) = (L2 . v);

      compatibility ;

    end

    definition

      let V be non empty addLoopStr;

      let L1,L2 be Linear_Combination of V;

      :: original: +

      redefine

      :: RLVECT_2:def10

      func L1 + L2 -> Linear_Combination of V means

      : Def10: for v be Element of V holds (it . v) = ((L1 . v) + (L2 . v));

      coherence

      proof

        reconsider f = (L1 + L2) as Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

        now

          let v be Element of V;

          assume

           A1: not v in (( Carrier L1) \/ ( Carrier L2));

          then not v in ( Carrier L2) by XBOOLE_0:def 3;

          then

           A2: (L2 . v) = 0 ;

           not v in ( Carrier L1) by A1, XBOOLE_0:def 3;

          then (L1 . v) = 0 ;

          

          hence (f . v) = ( 0 + 0 ) by A2, VALUED_1: 1

          .= 0 ;

        end;

        hence thesis by Def3;

      end;

      compatibility

      proof

        let f be Linear_Combination of V;

        thus f = (L1 + L2) implies for v be Element of V holds (f . v) = ((L1 . v) + (L2 . v)) by VALUED_1: 1;

        assume

         A3: for v be Element of V holds (f . v) = ((L1 . v) + (L2 . v));

        thus f = (L1 + L2)

        proof

          let v be Element of the carrier of V;

          

          thus (f . v) = ((L1 . v) + (L2 . v)) by A3

          .= ((L1 + L2) . v) by VALUED_1: 1;

        end;

      end;

    end

    theorem :: RLVECT_2:37

    

     Th37: ( Carrier (L1 + L2)) c= (( Carrier L1) \/ ( Carrier L2))

    proof

      let x be object;

      assume x in ( Carrier (L1 + L2));

      then

      consider u such that

       A1: x = u and

       A2: ((L1 + L2) . u) <> 0 ;

      ((L1 + L2) . u) = ((L1 . u) + (L2 . u)) by Def10;

      then (L1 . u) <> 0 or (L2 . u) <> 0 by A2;

      then x in { v1 : (L1 . v1) <> 0 } or x in { v2 : (L2 . v2) <> 0 } by A1;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: RLVECT_2:38

    

     Th38: L1 is Linear_Combination of A & L2 is Linear_Combination of A implies (L1 + L2) is Linear_Combination of A

    proof

      assume L1 is Linear_Combination of A & L2 is Linear_Combination of A;

      then ( Carrier L1) c= A & ( Carrier L2) c= A by Def6;

      then

       A1: (( Carrier L1) \/ ( Carrier L2)) c= A by XBOOLE_1: 8;

      ( Carrier (L1 + L2)) c= (( Carrier L1) \/ ( Carrier L2)) by Th37;

      hence ( Carrier (L1 + L2)) c= A by A1;

    end;

    theorem :: RLVECT_2:39

    for V be non empty addLoopStr, L1,L2 be Linear_Combination of V holds (L1 + L2) = (L2 + L1);

    theorem :: RLVECT_2:40

    

     Th40: (L1 + (L2 + L3)) = ((L1 + L2) + L3)

    proof

      let v;

      

      thus ((L1 + (L2 + L3)) . v) = ((L1 . v) + ((L2 + L3) . v)) by Def10

      .= ((L1 . v) + ((L2 . v) + (L3 . v))) by Def10

      .= (((L1 . v) + (L2 . v)) + (L3 . v))

      .= (((L1 + L2) . v) + (L3 . v)) by Def10

      .= (((L1 + L2) + L3) . v) by Def10;

    end;

    theorem :: RLVECT_2:41

    

     Th41: (L + ( ZeroLC V)) = L & (( ZeroLC V) + L) = L

    proof

      thus (L + ( ZeroLC V)) = L

      proof

        let v;

        

        thus ((L + ( ZeroLC V)) . v) = ((L . v) + (( ZeroLC V) . v)) by Def10

        .= ((L . v) + 0 ) by Th20

        .= (L . v);

      end;

      hence thesis;

    end;

    definition

      let V;

      let a be Real;

      let L;

      :: RLVECT_2:def11

      func a * L -> Linear_Combination of V means

      : Def11: for v holds (it . v) = (a * (L . v));

      existence

      proof

        deffunc F( Element of V) = ( In ((a * (L . $1)), REAL ));

        consider f be Function of the carrier of V, REAL such that

         A1: for v be Element of V holds (f . v) = F(v) from FUNCT_2:sch 4;

        reconsider f as Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

        now

          let v;

          assume not v in ( Carrier L);

          then

           A2: (L . v) = 0 ;

          

          thus (f . v) = F(v) by A1

          .= (a * 0 ) by A2

          .= 0 ;

        end;

        then

        reconsider f as Linear_Combination of V by Def3;

        take f;

        let v;

        (f . v) = F(v) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let L1, L2;

        assume

         A3: for v holds (L1 . v) = (a * (L . v));

        assume

         A4: for v holds (L2 . v) = (a * (L . v));

        let v;

        

        thus (L1 . v) = (a * (L . v)) by A3

        .= (L2 . v) by A4;

      end;

    end

    theorem :: RLVECT_2:42

    

     Th42: a <> 0 implies ( Carrier (a * L)) = ( Carrier L)

    proof

      set T = { u : ((a * L) . u) <> 0 };

      set S = { v : (L . v) <> 0 };

      assume

       A1: a <> 0 ;

      T = S

      proof

        thus T c= S

        proof

          let x be object;

          assume x in T;

          then

          consider u such that

           A2: x = u and

           A3: ((a * L) . u) <> 0 ;

          ((a * L) . u) = (a * (L . u)) by Def11;

          then (L . u) <> 0 by A3;

          hence thesis by A2;

        end;

        let x be object;

        assume x in S;

        then

        consider v such that

         A4: x = v and

         A5: (L . v) <> 0 ;

        ((a * L) . v) = (a * (L . v)) by Def11;

        then ((a * L) . v) <> 0 by A1, A5, XCMPLX_1: 6;

        hence thesis by A4;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_2:43

    

     Th43: ( 0 * L) = ( ZeroLC V)

    proof

      let v;

      

      thus (( 0 * L) . v) = ( 0 * (L . v)) by Def11

      .= (( ZeroLC V) . v) by Th20;

    end;

    theorem :: RLVECT_2:44

    

     Th44: L is Linear_Combination of A implies (a * L) is Linear_Combination of A

    proof

      assume

       A1: L is Linear_Combination of A;

      now

        per cases ;

          suppose a = 0 ;

          then (a * L) = ( ZeroLC V) by Th43;

          hence thesis by Th22;

        end;

          suppose a <> 0 ;

          then ( Carrier (a * L)) = ( Carrier L) by Th42;

          hence thesis by A1, Def6;

        end;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_2:45

    

     Th45: ((a + b) * L) = ((a * L) + (b * L))

    proof

      let v;

      

      thus (((a + b) * L) . v) = ((a + b) * (L . v)) by Def11

      .= ((a * (L . v)) + (b * (L . v)))

      .= (((a * L) . v) + (b * (L . v))) by Def11

      .= (((a * L) . v) + ((b * L) . v)) by Def11

      .= (((a * L) + (b * L)) . v) by Def10;

    end;

    theorem :: RLVECT_2:46

    

     Th46: (a * (L1 + L2)) = ((a * L1) + (a * L2))

    proof

      let v;

      

      thus ((a * (L1 + L2)) . v) = (a * ((L1 + L2) . v)) by Def11

      .= (a * ((L1 . v) + (L2 . v))) by Def10

      .= ((a * (L1 . v)) + (a * (L2 . v)))

      .= (((a * L1) . v) + (a * (L2 . v))) by Def11

      .= (((a * L1) . v) + ((a * L2) . v)) by Def11

      .= (((a * L1) + (a * L2)) . v) by Def10;

    end;

    theorem :: RLVECT_2:47

    

     Th47: (a * (b * L)) = ((a * b) * L)

    proof

      let v;

      

      thus ((a * (b * L)) . v) = (a * ((b * L) . v)) by Def11

      .= (a * (b * (L . v))) by Def11

      .= ((a * b) * (L . v))

      .= (((a * b) * L) . v) by Def11;

    end;

    theorem :: RLVECT_2:48

    

     Th48: (1 * L) = L

    proof

      let v;

      

      thus ((1 * L) . v) = (1 * (L . v)) by Def11

      .= (L . v);

    end;

    definition

      let V, L;

      :: RLVECT_2:def12

      func - L -> Linear_Combination of V equals (( - 1) * L);

      correctness ;

    end

    theorem :: RLVECT_2:49

    

     Th49: (( - L) . v) = ( - (L . v))

    proof

      

      thus (( - L) . v) = (( - 1) * (L . v)) by Def11

      .= ( - (L . v));

    end;

    theorem :: RLVECT_2:50

    (L1 + L2) = ( ZeroLC V) implies L2 = ( - L1)

    proof

      assume

       A1: (L1 + L2) = ( ZeroLC V);

      let v;

      ((L1 . v) + (L2 . v)) = (( ZeroLC V) . v) by A1, Def10

      .= 0 by Th20;

      

      hence (L2 . v) = ( - (L1 . v))

      .= (( - L1) . v) by Th49;

    end;

    theorem :: RLVECT_2:51

    ( Carrier ( - L)) = ( Carrier L) by Th42;

    theorem :: RLVECT_2:52

    L is Linear_Combination of A implies ( - L) is Linear_Combination of A by Th44;

    theorem :: RLVECT_2:53

    ( - ( - L)) = L

    proof

      let v;

      

      thus (( - ( - L)) . v) = (((( - 1) * ( - 1)) * L) . v) by Th47

      .= (1 * (L . v)) by Def11

      .= (L . v);

    end;

    definition

      let V;

      let L1, L2;

      :: RLVECT_2:def13

      func L1 - L2 -> Linear_Combination of V equals (L1 + ( - L2));

      correctness ;

    end

    theorem :: RLVECT_2:54

    

     Th54: ((L1 - L2) . v) = ((L1 . v) - (L2 . v))

    proof

      

      thus ((L1 - L2) . v) = ((L1 . v) + (( - L2) . v)) by Def10

      .= ((L1 . v) + ( - (L2 . v))) by Th49

      .= ((L1 . v) - (L2 . v));

    end;

    theorem :: RLVECT_2:55

    ( Carrier (L1 - L2)) c= (( Carrier L1) \/ ( Carrier L2))

    proof

      ( Carrier (L1 - L2)) c= (( Carrier L1) \/ ( Carrier ( - L2))) by Th37;

      hence thesis by Th42;

    end;

    theorem :: RLVECT_2:56

    L1 is Linear_Combination of A & L2 is Linear_Combination of A implies (L1 - L2) is Linear_Combination of A

    proof

      assume that

       A1: L1 is Linear_Combination of A and

       A2: L2 is Linear_Combination of A;

      ( - L2) is Linear_Combination of A by A2, Th44;

      hence thesis by A1, Th38;

    end;

    theorem :: RLVECT_2:57

    

     Th57: (L - L) = ( ZeroLC V)

    proof

      let v;

      

      thus ((L - L) . v) = ((L . v) - (L . v)) by Th54

      .= (( ZeroLC V) . v) by Th20;

    end;

    definition

      let V;

      :: RLVECT_2:def14

      func LinComb (V) -> set means

      : Def14: x in it iff x is Linear_Combination of V;

      existence

      proof

        defpred P[ object] means $1 is Linear_Combination of V;

        consider A be set such that

         A1: for x be object holds x in A iff x in ( Funcs (the carrier of V, REAL )) & P[x] from XBOOLE_0:sch 1;

        take A;

        let x;

        thus x in A implies x is Linear_Combination of V by A1;

        assume x is Linear_Combination of V;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let D1,D2 be set;

        assume

         A2: for x holds x in D1 iff x is Linear_Combination of V;

        assume

         A3: for x holds x in D2 iff x is Linear_Combination of V;

        thus D1 c= D2

        proof

          let x be object;

          assume x in D1;

          then x is Linear_Combination of V by A2;

          hence thesis by A3;

        end;

        let x be object;

        assume x in D2;

        then x is Linear_Combination of V by A3;

        hence thesis by A2;

      end;

    end

    registration

      let V;

      cluster ( LinComb V) -> non empty;

      coherence

      proof

        set x = the Linear_Combination of V;

        x in ( LinComb V) by Def14;

        hence thesis;

      end;

    end

    reserve e,e1,e2 for Element of ( LinComb V);

    definition

      let V;

      let e;

      :: RLVECT_2:def15

      func @ e -> Linear_Combination of V equals e;

      coherence by Def14;

    end

    definition

      let V;

      let L;

      :: RLVECT_2:def16

      func @ L -> Element of ( LinComb V) equals L;

      coherence by Def14;

    end

    definition

      let V;

      :: RLVECT_2:def17

      func LCAdd (V) -> BinOp of ( LinComb V) means

      : Def17: for e1, e2 holds (it . (e1,e2)) = (( @ e1) + ( @ e2));

      existence

      proof

        deffunc F( Element of ( LinComb V), Element of ( LinComb V)) = ( @ (( @ $1) + ( @ $2)));

        consider o be BinOp of ( LinComb V) such that

         A1: for e1, e2 holds (o . (e1,e2)) = F(e1,e2) from BINOP_1:sch 4;

        take o;

        let e1, e2;

        

        thus (o . (e1,e2)) = ( @ (( @ e1) + ( @ e2))) by A1

        .= (( @ e1) + ( @ e2));

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of ( LinComb V);

        assume

         A2: for e1, e2 holds (o1 . (e1,e2)) = (( @ e1) + ( @ e2));

        assume

         A3: for e1, e2 holds (o2 . (e1,e2)) = (( @ e1) + ( @ e2));

        now

          let e1, e2;

          

          thus (o1 . (e1,e2)) = (( @ e1) + ( @ e2)) by A2

          .= (o2 . (e1,e2)) by A3;

        end;

        hence thesis;

      end;

    end

    definition

      let V;

      :: RLVECT_2:def18

      func LCMult (V) -> Function of [: REAL , ( LinComb V):], ( LinComb V) means

      : Def18: for a, e holds (it . [a, e]) = (a * ( @ e));

      existence

      proof

        defpred P[ Real, Element of ( LinComb V), set] means ex a st a = $1 & $3 = (a * ( @ $2));

        

         A1: for x be Element of REAL , e1 holds ex e2 st P[x, e1, e2]

        proof

          let x be Element of REAL , e1;

          take ( @ (x * ( @ e1)));

          take x;

          thus thesis;

        end;

        consider g be Function of [: REAL , ( LinComb V):], ( LinComb V) such that

         A2: for x be Element of REAL , e holds P[x, e, (g . (x,e))] from BINOP_1:sch 3( A1);

        take g;

        let a, e;

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

        ex b st b = aa & (g . (aa,e)) = (b * ( @ e)) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let g1,g2 be Function of [: REAL , ( LinComb V):], ( LinComb V);

        assume

         A3: for a, e holds (g1 . [a, e]) = (a * ( @ e));

        assume

         A4: for a, e holds (g2 . [a, e]) = (a * ( @ e));

        now

          let x be Element of REAL , e;

          

          thus (g1 . (x,e)) = (x * ( @ e)) by A3

          .= (g2 . (x,e)) by A4;

        end;

        hence thesis;

      end;

    end

    definition

      let V;

      :: RLVECT_2:def19

      func LC_RLSpace V -> RLSStruct equals RLSStruct (# ( LinComb V), ( @ ( ZeroLC V)), ( LCAdd V), ( LCMult V) #);

      coherence ;

    end

    registration

      let V;

      cluster ( LC_RLSpace V) -> strict non empty;

      coherence ;

    end

    registration

      let V;

      cluster ( LC_RLSpace V) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence

      proof

        set S = ( LC_RLSpace V);

         A1:

        now

          let v,u be VECTOR of S, K, L;

          

           A2: ( @ ( @ K)) = K & ( @ ( @ L)) = L;

          assume v = K & u = L;

          hence (v + u) = (K + L) by A2, Def17;

        end;

        thus S is Abelian

        proof

          let u,v be Element of S;

          reconsider K = u, L = v as Linear_Combination of V by Def14;

          

          thus (u + v) = (L + K) by A1

          .= (v + u) by A1;

        end;

        thus S is add-associative

        proof

          let u,v,w be Element of S;

          reconsider L = u, K = v, M = w as Linear_Combination of V by Def14;

          

           A3: (v + w) = (K + M) by A1;

          (u + v) = (L + K) by A1;

          

          hence ((u + v) + w) = ((L + K) + M) by A1

          .= (L + (K + M)) by Th40

          .= (u + (v + w)) by A1, A3;

        end;

        thus S is right_zeroed

        proof

          let v be Element of S;

          reconsider K = v as Linear_Combination of V by Def14;

          

          thus (v + ( 0. S)) = (K + ( ZeroLC V)) by A1

          .= v by Th41;

        end;

        thus S is right_complementable

        proof

          let v be Element of S;

          reconsider K = v as Linear_Combination of V by Def14;

          ( - K) in the carrier of S by Def14;

          then ( - K) in S;

          then ( - K) = ( vector (S,( - K))) by Def1;

          

          then (v + ( vector (S,( - K)))) = (K - K) by A1

          .= ( 0. S) by Th57;

          hence ex w be VECTOR of S st (v + w) = ( 0. S);

        end;

         A4:

        now

          let v be VECTOR of S, L, a;

          

           A5: ( @ ( @ L)) = L;

          assume v = L;

          hence (a * v) = (a * L) by A5, Def18;

        end;

        thus for a be Real holds for v,w be VECTOR of S holds (a * (v + w)) = ((a * v) + (a * w))

        proof

          let a be Real;

          let v,w be VECTOR of S;

          reconsider K = v, M = w as Linear_Combination of V by Def14;

          reconsider a as Real;

          

           A6: (a * v) = (a * K) & (a * w) = (a * M) by A4;

          (v + w) = (K + M) by A1;

          

          then (a * (v + w)) = (a * (K + M)) by A4

          .= ((a * K) + (a * M)) by Th46

          .= ((a * v) + (a * w)) by A1, A6;

          hence thesis;

        end;

        thus for a,b be Real holds for v be VECTOR of S holds ((a + b) * v) = ((a * v) + (b * v))

        proof

          let a,b be Real;

          let v be VECTOR of S;

          reconsider K = v as Linear_Combination of V by Def14;

          reconsider a, b as Real;

          

           A7: (a * v) = (a * K) & (b * v) = (b * K) by A4;

          ((a + b) * v) = ((a + b) * K) by A4

          .= ((a * K) + (b * K)) by Th45

          .= ((a * v) + (b * v)) by A1, A7;

          hence thesis;

        end;

        thus for a,b be Real holds for v be VECTOR of S holds ((a * b) * v) = (a * (b * v))

        proof

          let a,b be Real;

          let v be VECTOR of S;

          reconsider K = v as Linear_Combination of V by Def14;

          reconsider a, b as Real;

          

           A8: (b * v) = (b * K) by A4;

          ((a * b) * v) = ((a * b) * K) by A4

          .= (a * (b * K)) by Th47

          .= (a * (b * v)) by A4, A8;

          hence thesis;

        end;

        let v be VECTOR of S;

        reconsider K = v as Linear_Combination of V by Def14;

        

        thus (1 * v) = (1 * K) by A4

        .= v by Th48;

      end;

    end

    theorem :: RLVECT_2:58

    the carrier of ( LC_RLSpace V) = ( LinComb V);

    theorem :: RLVECT_2:59

    ( 0. ( LC_RLSpace V)) = ( ZeroLC V);

    theorem :: RLVECT_2:60

    the addF of ( LC_RLSpace V) = ( LCAdd V);

    theorem :: RLVECT_2:61

    the Mult of ( LC_RLSpace V) = ( LCMult V);

    theorem :: RLVECT_2:62

    

     Th62: (( vector (( LC_RLSpace V),L1)) + ( vector (( LC_RLSpace V),L2))) = (L1 + L2)

    proof

      set v2 = ( vector (( LC_RLSpace V),L2));

      

       A1: L1 = ( @ ( @ L1)) & L2 = ( @ ( @ L2));

      L2 in the carrier of ( LC_RLSpace V) by Def14;

      then

       A2: L2 in ( LC_RLSpace V);

      L1 in the carrier of ( LC_RLSpace V) by Def14;

      then L1 in ( LC_RLSpace V);

      

      hence (( vector (( LC_RLSpace V),L1)) + ( vector (( LC_RLSpace V),L2))) = (( LCAdd V) . [L1, v2]) by Def1

      .= (( LCAdd V) . (( @ L1),( @ L2))) by A2, Def1

      .= (L1 + L2) by A1, Def17;

    end;

    theorem :: RLVECT_2:63

    

     Th63: (a * ( vector (( LC_RLSpace V),L))) = (a * L)

    proof

      

       A1: ( @ ( @ L)) = L;

      L in the carrier of ( LC_RLSpace V) by Def14;

      then L in ( LC_RLSpace V);

      

      hence (a * ( vector (( LC_RLSpace V),L))) = (( LCMult V) . [a, ( @ L)]) by Def1

      .= (a * L) by A1, Def18;

    end;

    theorem :: RLVECT_2:64

    

     Th64: ( - ( vector (( LC_RLSpace V),L))) = ( - L)

    proof

      

      thus ( - ( vector (( LC_RLSpace V),L))) = (( - 1) * ( vector (( LC_RLSpace V),L))) by RLVECT_1: 16

      .= ( - L) by Th63;

    end;

    theorem :: RLVECT_2:65

    (( vector (( LC_RLSpace V),L1)) - ( vector (( LC_RLSpace V),L2))) = (L1 - L2)

    proof

      ( - L2) in ( LinComb V) by Def14;

      then

       A1: ( - L2) in ( LC_RLSpace V);

      ( - ( vector (( LC_RLSpace V),L2))) = ( - L2) by Th64

      .= ( vector (( LC_RLSpace V),( - L2))) by A1, Def1;

      hence thesis by Th62;

    end;

    definition

      let V;

      let A;

      :: RLVECT_2:def20

      func LC_RLSpace (A) -> strict Subspace of ( LC_RLSpace V) means the carrier of it = the set of all l;

      existence

      proof

        set X = the set of all l;

        X c= the carrier of ( LC_RLSpace V)

        proof

          let x be object;

          assume x in X;

          then ex l st x = l;

          hence thesis by Def14;

        end;

        then

        reconsider X as Subset of ( LC_RLSpace V);

        

         A1: X is linearly-closed

        proof

          thus for v,u be VECTOR of ( LC_RLSpace V) st v in X & u in X holds (v + u) in X

          proof

            let v,u be VECTOR of ( LC_RLSpace V);

            assume that

             A2: v in X and

             A3: u in X;

            consider l1 such that

             A4: v = l1 by A2;

            consider l2 such that

             A5: u = l2 by A3;

            

             A6: u = ( vector (( LC_RLSpace V),l2)) by A5, Def1, RLVECT_1: 1;

            v = ( vector (( LC_RLSpace V),l1)) by A4, Def1, RLVECT_1: 1;

            then (v + u) = (l1 + l2) by A6, Th62;

            then (v + u) is Linear_Combination of A by Th38;

            hence thesis;

          end;

          let a be Real;

          let v be VECTOR of ( LC_RLSpace V);

          assume v in X;

          then

          consider l such that

           A7: v = l;

          (a * v) = (a * ( vector (( LC_RLSpace V),l))) by A7, Def1, RLVECT_1: 1

          .= (a * l) by Th63;

          then (a * v) is Linear_Combination of A by Th44;

          hence thesis;

        end;

        ( ZeroLC V) is Linear_Combination of A by Th22;

        then ( ZeroLC V) in X;

        hence thesis by A1, RLSUB_1: 35;

      end;

      uniqueness by RLSUB_1: 30;

    end

    reserve x,y for set,

k,n for Nat;

    theorem :: RLVECT_2:66

    

     Th66: for R be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, a be Element of R holds for V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over R, 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) = (a * v) holds ( Sum F) = (a * ( Sum G))

    proof

      let R be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, a be Element of R;

      let V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over R, F,G be FinSequence of V;

      defpred P[ Nat] 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 ( dom H) & v = (I . k) holds (H . k) = (a * v)) holds ( Sum H) = (a * ( Sum I));

      

       A1: P[n] implies P[(n + 1)]

      proof

        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 ( dom H) & v = (I . k) holds (H . k) = (a * v) holds ( Sum H) = (a * ( 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 ( dom H) & v = (I . k) holds (H . k) = (a * v);

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

        

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

        then

         A7: q = (I | ( dom q)) by A3, A4, FINSEQ_1: 17;

        

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

        

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

         A10:

        now

          

           A11: ( dom p) c= ( dom H) by A4, A6, A8, FINSEQ_3: 30;

          let k;

          let v be Element of V;

          assume that

           A12: k in ( dom p) and

           A13: v = (q . k);

          ( dom q) = ( dom p) by A8, A9, FINSEQ_3: 29;

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

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

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

        end;

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

        then

         A14: (n + 1) in ( dom H) by A4, FINSEQ_1:def 3;

        ( dom H) = ( dom I) by A3, FINSEQ_3: 29;

        then

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

        

         A15: v1 = (a * v2) by A5, A14;

        p = (H | ( dom p)) by A4, A6, FINSEQ_1: 17;

        

        hence ( Sum H) = (( Sum p) + v1) by A4, A8, RLVECT_1: 38

        .= ((a * ( Sum q)) + (a * v2)) by A2, A8, A9, A10, A15

        .= (a * (( Sum q) + v2)) by VECTSP_1:def 14

        .= (a * ( Sum I)) by A3, A4, A9, A7, RLVECT_1: 38;

      end;

      

       A16: P[ 0 ]

      proof

        let H,I be FinSequence of V;

        assume that

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

         A18: ( len H) = 0 and for k holds for v be Element of V st k in ( dom H) & v = (I . k) holds (H . k) = (a * v);

        H = ( <*> the carrier of V) by A18;

        then

         A19: ( Sum H) = ( 0. V) by RLVECT_1: 43;

        I = ( <*> the carrier of V) by A17, A18;

        then ( Sum I) = ( 0. V) by RLVECT_1: 43;

        hence thesis by A19, VECTSP_1: 14;

      end;

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

      hence thesis;

    end;

    theorem :: RLVECT_2:67

    for R be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, a be Element of R holds for V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over R, F,G be FinSequence of V st ( len F) = ( len G) & for k st k in ( dom F) holds (G . k) = (a * (F /. k)) holds ( Sum G) = (a * ( Sum F))

    proof

      let R be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, a be Element of R;

      let V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over R, F,G be FinSequence of V;

      assume that

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

       A2: for k st k in ( dom F) holds (G . k) = (a * (F /. k));

      now

        let k;

        let v be Element of V;

        assume that

         A3: k in ( dom G) and

         A4: v = (F . k);

        

         A5: k in ( dom F) by A1, A3, FINSEQ_3: 29;

        then v = (F /. k) by A4, PARTFUN1:def 6;

        hence (G . k) = (a * v) by A2, A5;

      end;

      hence thesis by A1, Th66;

    end;

    theorem :: RLVECT_2:68

    for R be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V be Abelian add-associative right_zeroed right_complementable non empty ModuleStr over R, F,G,H be FinSequence of V st ( len F) = ( len G) & ( len F) = ( len H) & for k st k in ( dom F) holds (H . k) = ((F /. k) - (G /. k)) holds ( Sum H) = (( Sum F) - ( Sum G))

    proof

      let R be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr;

      let V be Abelian add-associative right_zeroed right_complementable non empty ModuleStr over R, F,G,H be FinSequence of V;

      assume that

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

       A2: ( len F) = ( len H) and

       A3: for k st k in ( dom F) holds (H . k) = ((F /. k) - (G /. k));

      deffunc F( Nat) = ( - (G /. $1));

      consider I be FinSequence such that

       A4: ( len I) = ( len G) and

       A5: for k be Nat st k in ( dom I) holds (I . k) = F(k) from FINSEQ_1:sch 2;

      

       A6: ( dom I) = ( Seg ( len G)) by A4, FINSEQ_1:def 3;

      then

       A7: for k st k in ( Seg ( len G)) holds (I . k) = F(k) by A5;

      ( rng I) c= the carrier of V

      proof

        let x be object;

        assume x in ( rng I);

        then

        consider y be object such that

         A8: y in ( dom I) and

         A9: (I . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A8;

        x = ( - (G /. y)) by A5, A8, A9;

        then

        reconsider v = x as Element of V;

        v in V;

        hence thesis;

      end;

      then

      reconsider I as FinSequence of V by FINSEQ_1:def 4;

      

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

      now

        let k;

        

         A11: ( dom F) = ( dom G) by A1, FINSEQ_3: 29;

        assume

         A12: k in ( dom F);

        then k in ( dom I) by A1, A4, FINSEQ_3: 29;

        then

         A13: (I . k) = (I /. k) by PARTFUN1:def 6;

        

        thus (H . k) = ((F /. k) - (G /. k)) by A3, A12

        .= ((F /. k) + ( - (G /. k)))

        .= ((F /. k) + (I /. k)) by A5, A6, A10, A12, A13, A11;

      end;

      then

       A14: ( Sum H) = (( Sum F) + ( Sum I)) by A1, A2, A4, Th2;

      ( Sum I) = ( - ( Sum G)) by A4, A7, A10, Th4;

      hence thesis by A14;

    end;

    theorem :: RLVECT_2:69

    for R be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, a be Element of R holds for V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over R holds (a * ( Sum ( <*> the carrier of V))) = ( 0. V)

    proof

      let R be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, a be Element of R;

      let V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over R;

      

      thus (a * ( Sum ( <*> the carrier of V))) = (a * ( 0. V)) by RLVECT_1: 43

      .= ( 0. V) by VECTSP_1: 14;

    end;

    theorem :: RLVECT_2:70

    for R be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, a be Element of R holds for V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over R, v,u be Element of V holds (a * ( Sum <*v, u*>)) = ((a * v) + (a * u))

    proof

      let R be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, a be Element of R;

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

      

      thus (a * ( Sum <*v, u*>)) = (a * (v + u)) by RLVECT_1: 45

      .= ((a * v) + (a * u)) by VECTSP_1:def 14;

    end;

    theorem :: RLVECT_2:71

    for R be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, a be Element of R holds for V be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over R, v,u,w be Element of V holds (a * ( Sum <*v, u, w*>)) = (((a * v) + (a * u)) + (a * w))

    proof

      let R be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, a be Element of R;

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

      

      thus (a * ( Sum <*v, u, w*>)) = (a * ((v + u) + w)) by RLVECT_1: 46

      .= ((a * (v + u)) + (a * w)) by VECTSP_1:def 14

      .= (((a * v) + (a * u)) + (a * w)) by VECTSP_1:def 14;

    end;