rlvect_x.miz



    begin

    reconsider z0 = 0 as Real;

    deffunc H( object) = ( In ( 0 , REAL ));

    theorem :: RLVECT_X:1

    for X be RealLinearSpace, R1,R2 be FinSequence of X st ( len R1) = ( len R2) holds ( Sum (R1 + R2)) = (( Sum R1) + ( Sum R2))

    proof

      let X be RealLinearSpace, R1,R2 be FinSequence of X;

      assume ( len R1) = ( len R2);

      then ( dom R1) = ( dom R2) by FINSEQ_3: 29;

      hence thesis by BINOM: 7;

    end;

    theorem :: RLVECT_X:2

    for X be RealLinearSpace, R1,R2,R3 be FinSequence of X st ( len R1) = ( len R2) & R3 = (R1 - R2) holds ( Sum R3) = (( Sum R1) - ( Sum R2))

    proof

      let X be RealLinearSpace, R1,R2,R3 be FinSequence of X;

      assume

       A1: ( len R1) = ( len R2) & R3 = (R1 - R2);

      then

       A2: ( dom R1) = ( dom R2) by FINSEQ_3: 29;

      

       A3: ( dom R3) = (( dom R1) /\ ( dom R2)) by A1, VFUNCT_1:def 2

      .= ( dom R1) by A2;

      then

       A4: ( len R3) = ( len R1) by FINSEQ_3: 29;

      for k be Nat st k in ( dom R1) holds (R3 . k) = ((R1 /. k) - (R2 /. k))

      proof

        let k be Nat;

        assume

         A5: k in ( dom R1);

        

        hence (R3 . k) = (R3 /. k) by A3, PARTFUN1:def 6

        .= ((R1 /. k) - (R2 /. k)) by A1, A5, A3, VFUNCT_1:def 2;

      end;

      hence thesis by A1, A4, RLVECT_2: 5;

    end;

    theorem :: RLVECT_X:3

    

     Th3: for X be RealLinearSpace, R1,R2 be FinSequence of X, a be Element of REAL st R2 = (a (#) R1) holds ( Sum R2) = (a * ( Sum R1))

    proof

      let X be RealLinearSpace, R1,R2 be FinSequence of X, a be Element of REAL ;

      assume

       A1: R2 = (a (#) R1);

      ( dom R2) = ( dom R1) by A1, VFUNCT_1:def 4;

      then

       A2: ( len R2) = ( len R1) by FINSEQ_3: 29;

      for k be Nat st k in ( dom R1) holds (R2 . k) = (a * (R1 /. k))

      proof

        let k be Nat;

        assume k in ( dom R1);

        then

         A3: k in ( dom R2) by A1, VFUNCT_1:def 4;

        

        hence (R2 . k) = (R2 /. k) by PARTFUN1:def 6

        .= (a * (R1 /. k)) by A3, A1, VFUNCT_1:def 4;

      end;

      hence thesis by A2, RLVECT_2: 3;

    end;

    begin

    reserve x,y for set;

    reserve a,b for Real;

    reserve i,j for Integer;

    reserve V for RealLinearSpace;

    reserve W1,W2,W3 for Subspace of V;

    reserve v,v1,v2,v3,u,w,w1,w2,w3 for VECTOR of V;

    reserve A,B,C for Subset of V;

    reserve L,L1,L2 for Linear_Combination of V;

    reserve l,l1,l2 for Linear_Combination of A;

    definition

      let V, i, L;

      :: RLVECT_X:def1

      func i * L -> Linear_Combination of V means

      : Def1: for v holds (it . v) = (i * (L . v));

      existence

      proof

        deffunc F( Element of V) = ( In ((i * (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 be Element of V;

          assume not v in ( Carrier L);

          then

           A2: (L . v) = 0 ;

          

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

          .= 0 by A2;

        end;

        then

        reconsider f as Linear_Combination of V by RLVECT_2:def 3;

        take f;

        let v;

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

        hence thesis;

      end;

      uniqueness

      proof

        let L1, L2;

        assume that

         A3: for v holds (L1 . v) = (i * (L . v)) and

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

        let v;

        

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

        .= (L2 . v) by A4;

      end;

    end

    definition

      let V, A;

      :: RLVECT_X:def2

      func Z_Lin (A) -> Subset of V equals { ( Sum l) : ( rng l) c= INT };

      correctness

      proof

        set A1 = { ( Sum l) : ( rng l) c= INT };

        A1 c= the carrier of V

        proof

          let x be object;

          assume x in A1;

          then ex l st x = ( Sum l) & ( rng l) c= INT ;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: RLVECT_X:4

    

     Th4: a = i implies (a * l) = (i * l)

    proof

      assume

       A1: a = i;

      for v be VECTOR of V holds ((i * l) . v) = (a * (l . v)) by A1, Def1;

      hence thesis by RLVECT_2:def 11;

    end;

    theorem :: RLVECT_X:5

    

     Th5: ( rng l1) c= INT & ( rng l2) c= INT implies ( rng (l1 + l2)) c= INT

    proof

      assume

       A1: ( rng l1) c= INT & ( rng l2) c= INT ;

      let y be object;

      assume

       A2: y in ( rng (l1 + l2));

      consider x be object such that

       A3: x in the carrier of V & y = ((l1 + l2) . x) by A2, FUNCT_2: 11;

      reconsider z = x as VECTOR of V by A3;

      (l1 . z) in ( rng l1) by FUNCT_2: 4;

      then

      reconsider z1 = (l1 . z) as Integer by A1;

      (l2 . z) in ( rng l2) by FUNCT_2: 4;

      then

      reconsider z2 = (l2 . z) as Integer by A1;

      ((l1 + l2) . z) = (z1 + z2) by RLVECT_2:def 10;

      hence y in INT by A3, INT_1:def 2;

    end;

    theorem :: RLVECT_X:6

    

     Th6: ( rng l) c= INT implies ( rng (i * l)) c= INT

    proof

      assume

       A1: ( rng l) c= INT ;

      let y be object;

      assume

       A2: y in ( rng (i * l));

      consider x be object such that

       A3: x in the carrier of V & y = ((i * l) . x) by A2, FUNCT_2: 11;

      reconsider z = x as VECTOR of V by A3;

      reconsider ii = i as Real;

      (l . z) in ( rng l) by FUNCT_2: 4;

      then

      reconsider z1 = (l . z) as Integer by A1;

      ((i * l) . z) = ((ii * l) . z) by Th4

      .= (i * z1) by RLVECT_2:def 11;

      hence y in INT by A3, INT_1:def 2;

    end;

    theorem :: RLVECT_X:7

    

     Th7: ( rng ( ZeroLC V)) c= INT

    proof

      let y be object;

      assume

       A1: y in ( rng ( ZeroLC V));

      consider x be object such that

       A2: x in the carrier of V & y = (( ZeroLC V) . x) by A1, FUNCT_2: 11;

      reconsider z = x as VECTOR of V by A2;

      (( ZeroLC V) . z) = 0 by RLVECT_2: 20;

      hence y in INT by A2, NUMBERS: 17;

    end;

    theorem :: RLVECT_X:8

    

     Th8: ( Z_Lin A) c= the carrier of ( Lin A)

    proof

      let x be object;

      assume x in ( Z_Lin A);

      then

      consider l1 be Linear_Combination of A such that

       A1: x = ( Sum l1) & ( rng l1) c= INT ;

      x in ( Lin A) by A1, RLVECT_3: 14;

      hence thesis by STRUCT_0:def 5;

    end;

    theorem :: RLVECT_X:9

    

     Th9: v in ( Z_Lin A) & u in ( Z_Lin A) implies (v + u) in ( Z_Lin A)

    proof

      assume that

       A1: v in ( Z_Lin A) and

       A2: u in ( Z_Lin A);

      consider l1 be Linear_Combination of A such that

       A3: v = ( Sum l1) & ( rng l1) c= INT by A1;

      consider l2 be Linear_Combination of A such that

       A4: u = ( Sum l2) & ( rng l2) c= INT by A2;

      reconsider f = (l1 + l2) as Linear_Combination of A by RLVECT_2: 38;

      

       A5: ( rng f) c= INT by A3, A4, Th5;

      (v + u) = ( Sum f) by A3, A4, RLVECT_3: 1;

      hence thesis by A5;

    end;

    theorem :: RLVECT_X:10

    

     Th10: v in ( Z_Lin A) implies (i * v) in ( Z_Lin A)

    proof

      assume v in ( Z_Lin A);

      then

      consider l such that

       A1: v = ( Sum l) & ( rng l) c= INT ;

      reconsider a = i as Real;

      

       A2: (a * l) = (i * l) by Th4;

      then

      reconsider f = (i * l) as Linear_Combination of A by RLVECT_2: 44;

      

       A3: (i * v) = ( Sum f) by A1, A2, RLVECT_3: 2;

      ( rng (i * l)) c= INT by Th6, A1;

      hence thesis by A3;

    end;

    theorem :: RLVECT_X:11

    

     Th11: ( 0. V) in ( Z_Lin A)

    proof

      reconsider l = ( ZeroLC V) as Linear_Combination of A by RLVECT_2: 22;

      

       A1: ( Sum l) = ( 0. V) by RLVECT_2: 30;

      ( rng l) c= INT by Th7;

      hence thesis by A1;

    end;

    theorem :: RLVECT_X:12

    

     Th12: x in A implies x in ( Z_Lin A)

    proof

      assume

       A1: x in A;

      then

      reconsider v = x as VECTOR of V;

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

       A2: (f . v) = ( In (1, REAL )) and

       A3: for u st u <> v holds (f . u) = H(u) from FUNCT_2:sch 6;

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

      ex T be finite Subset of V st for u st not u in T holds (f . u) = 0

      proof

        take T = {v};

        let u;

        assume not u in T;

        then u <> v by TARSKI:def 1;

        hence thesis by A3;

      end;

      then

      reconsider f as Linear_Combination of V by RLVECT_2:def 3;

      

       A4: ( Carrier f) c= {v}

      proof

        let x be object;

        assume x in ( Carrier f);

        then

        consider u such that

         A5: x = u and

         A6: (f . u) <> 0 ;

        u = v by A3, A6;

        hence thesis by A5, TARSKI:def 1;

      end;

      then

      reconsider f as Linear_Combination of {v} by RLVECT_2:def 6;

      

       A7: ( Sum f) = ((f . v) * v) by RLVECT_2: 32

      .= v by A2, RLVECT_1:def 8;

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

      then ( Carrier f) c= A by A4;

      then

      reconsider f as Linear_Combination of A by RLVECT_2:def 6;

      ( rng f) c= INT

      proof

        let y be object;

        assume

         A8: y in ( rng f);

        consider x be object such that

         A9: x in the carrier of V & y = (f . x) by A8, FUNCT_2: 11;

        reconsider z = x as VECTOR of V by A9;

        per cases ;

          suppose z <> v;

          then (f . z) = 0 by A3;

          hence y in INT by A9, NUMBERS: 17;

        end;

          suppose z = v;

          hence y in INT by A2, A9, NUMBERS: 17;

        end;

      end;

      hence thesis by A7;

    end;

    theorem :: RLVECT_X:13

    

     Th13: A c= B implies ( Z_Lin A) c= ( Z_Lin B)

    proof

      assume

       A1: A c= B;

      let v be object;

      assume v in ( Z_Lin A);

      then

      consider l such that

       A2: v = ( Sum l) & ( rng l) c= INT ;

      reconsider l as Linear_Combination of B by A1, RLVECT_2: 21;

      ( Sum l) = v by A2;

      hence v in ( Z_Lin B) by A2;

    end;

    theorem :: RLVECT_X:14

    ( Z_Lin (A \/ B)) = (( Z_Lin A) + ( Z_Lin B))

    proof

      now

        let v be object;

        assume v in ( Z_Lin (A \/ B));

        then

        consider l be Linear_Combination of (A \/ B) such that

         A1: v = ( Sum l) & ( rng l) c= INT ;

        deffunc F( object) = (l . $1);

        set D = (( Carrier l) \ A);

        set C = (( Carrier l) /\ A);

        defpred P[ object] means $1 in C;

        defpred D[ object] means $1 in D;

        

         A2: for x be object st x in the carrier of V holds ( P[x] implies F(x) in REAL ) & ( not P[x] implies H(x) in REAL ) by XREAL_0:def 1;

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

         A3: for x be object st x in the carrier of V holds ( P[x] implies (f . x) = F(x)) & ( not P[x] implies (f . x) = H(x)) from FUNCT_2:sch 5( A2);

        reconsider C as finite Subset of V;

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

        for u holds not u in C implies (f . u) = 0 by A3;

        then

        reconsider f as Linear_Combination of V by RLVECT_2:def 3;

        

         A4: ( rng f) c= INT

        proof

          let y be object;

          assume

           A5: y in ( rng f);

          consider x be object such that

           A6: x in the carrier of V & y = (f . x) by A5, FUNCT_2: 11;

          reconsider z = x as VECTOR of V by A6;

          per cases ;

            suppose not z in C;

            then (f . z) = 0 by A3;

            hence y in INT by A6, NUMBERS: 17;

          end;

            suppose z in C;

            then (f . z) = (l . z) by A3;

            then (f . z) in ( rng l) by FUNCT_2: 4;

            hence y in INT by A6, A1;

          end;

        end;

        

         A7: ( Carrier f) c= C

        proof

          let x be object;

          assume x in ( Carrier f);

          then

           A8: ex u st x = u & (f . u) <> 0 ;

          assume not x in C;

          hence thesis by A3, A8;

        end;

        C c= A by XBOOLE_1: 17;

        then ( Carrier f) c= A by A7;

        then

        reconsider f as Linear_Combination of A by RLVECT_2:def 6;

        

         A9: for x be object st x in the carrier of V holds ( D[x] implies F(x) in REAL ) & ( not D[x] implies H(x) in REAL ) by XREAL_0:def 1;

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

         A10: for x be object st x in the carrier of V holds ( D[x] implies (g . x) = F(x)) & ( not D[x] implies (g . x) = H(x)) from FUNCT_2:sch 5( A9);

        reconsider D as finite Subset of V;

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

        for u holds not u in D implies (g . u) = 0 by A10;

        then

        reconsider g as Linear_Combination of V by RLVECT_2:def 3;

        

         A11: ( rng g) c= INT

        proof

          let y be object;

          assume

           A12: y in ( rng g);

          consider x be object such that

           A13: x in the carrier of V & y = (g . x) by A12, FUNCT_2: 11;

          reconsider z = x as VECTOR of V by A13;

          per cases ;

            suppose not z in D;

            then (g . z) = 0 by A10;

            hence y in INT by A13, NUMBERS: 17;

          end;

            suppose z in D;

            then (g . z) = (l . z) by A10;

            then (g . z) in ( rng l) by FUNCT_2: 4;

            hence y in INT by A13, A1;

          end;

        end;

        

         A14: D c= B

        proof

          let x be object;

          assume x in D;

          then

           A15: x in ( Carrier l) & not x in A by XBOOLE_0:def 5;

          ( Carrier l) c= (A \/ B) by RLVECT_2:def 6;

          hence thesis by A15, XBOOLE_0:def 3;

        end;

        ( Carrier g) c= D

        proof

          let x be object;

          assume x in ( Carrier g);

          then

           A16: ex u st x = u & (g . u) <> 0 ;

          assume not x in D;

          hence thesis by A10, A16;

        end;

        then ( Carrier g) c= B by A14;

        then

        reconsider g as Linear_Combination of B by RLVECT_2:def 6;

        l = (f + g)

        proof

          let v;

          now

            per cases ;

              suppose

               A17: v in C;

               A18:

              now

                assume v in D;

                then not v in A by XBOOLE_0:def 5;

                hence contradiction by A17, XBOOLE_0:def 4;

              end;

              

              thus ((f + g) . v) = ((f . v) + (g . v)) by RLVECT_2:def 10

              .= ((l . v) + (g . v)) by A3, A17

              .= ((l . v) + z0) by A10, A18

              .= (l . v);

            end;

              suppose

               A19: not v in C;

              now

                per cases ;

                  suppose

                   A20: v in ( Carrier l);

                   A21:

                  now

                    assume not v in D;

                    then not v in ( Carrier l) or v in A by XBOOLE_0:def 5;

                    hence contradiction by A19, A20, XBOOLE_0:def 4;

                  end;

                  

                  thus ((f + g) . v) = ((f . v) + (g . v)) by RLVECT_2:def 10

                  .= (z0 + (g . v)) by A3, A19

                  .= (l . v) by A10, A21;

                end;

                  suppose

                   A22: not v in ( Carrier l);

                  then

                   A23: not v in D by XBOOLE_0:def 5;

                  

                   A24: not v in C by A22, XBOOLE_0:def 4;

                  

                  thus ((f + g) . v) = ((f . v) + (g . v)) by RLVECT_2:def 10

                  .= (z0 + (g . v)) by A3, A24

                  .= (z0 + z0) by A10, A23

                  .= (l . v) by A22;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        then

         A25: v = (( Sum f) + ( Sum g)) by A1, RLVECT_3: 1;

        ( Sum f) in ( Z_Lin A) & ( Sum g) in ( Z_Lin B) by A4, A11;

        hence v in (( Z_Lin A) + ( Z_Lin B)) by A25;

      end;

      then

       A26: ( Z_Lin (A \/ B)) c= (( Z_Lin A) + ( Z_Lin B));

      

       A27: ( Z_Lin A) c= ( Z_Lin (A \/ B)) & ( Z_Lin B) c= ( Z_Lin (A \/ B)) by Th13, XBOOLE_1: 7;

      now

        let x be object;

        assume x in (( Z_Lin A) + ( Z_Lin B));

        then

        consider u,v be Element of V such that

         A28: x = (u + v) & u in ( Z_Lin A) & v in ( Z_Lin B);

        thus x in ( Z_Lin (A \/ B)) by A28, A27, Th9;

      end;

      then (( Z_Lin A) + ( Z_Lin B)) c= ( Z_Lin (A \/ B));

      hence thesis by A26, XBOOLE_0:def 10;

    end;

    theorem :: RLVECT_X:15

    ( Z_Lin (A /\ B)) c= (( Z_Lin A) /\ ( Z_Lin B))

    proof

      ( Z_Lin (A /\ B)) c= ( Z_Lin A) & ( Z_Lin (A /\ B)) c= ( Z_Lin B) by Th13, XBOOLE_1: 17;

      hence thesis by XBOOLE_1: 19;

    end;

    theorem :: RLVECT_X:16

    

     Th16: x in ( Z_Lin {v}) iff ex a be Integer st x = (a * v)

    proof

      thus x in ( Z_Lin {v}) implies ex a be Integer st x = (a * v)

      proof

        assume x in ( Z_Lin {v});

        then

        consider l be Linear_Combination of {v} such that

         A1: x = ( Sum l) & ( rng l) c= INT ;

        

         A2: ( Sum l) = ((l . v) * v) by RLVECT_2: 32;

        ex f be Function st l = f & ( dom f) = the carrier of V & ( rng f) c= REAL by FUNCT_2:def 2;

        then (l . v) in ( rng l) by FUNCT_1: 3;

        hence thesis by A1, A2;

      end;

      given a0 be Integer such that

       A3: x = (a0 * v);

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

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

       A4: (f . v) = a and

       A5: for z be VECTOR of V st z <> v holds (f . z) = H(z) from FUNCT_2:sch 6;

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

       A6:

      now

        let z be VECTOR of V;

        assume not z in {v};

        then z <> v by TARSKI:def 1;

        hence (f . z) = 0 by A5;

      end;

      then

      reconsider f as Linear_Combination of V by RLVECT_2:def 3;

      ( Carrier f) c= {v}

      proof

        let x be object;

        assume

         A7: x in ( Carrier f);

        then (f . x) <> 0 by RLVECT_2: 19;

        then x = v by A5, A7;

        hence thesis by TARSKI:def 1;

      end;

      then

      reconsider f as Linear_Combination of {v} by RLVECT_2:def 6;

      

       A8: ( Sum f) = x by A3, A4, RLVECT_2: 32;

      ( rng f) c= INT

      proof

        let y be object;

        assume

         A9: y in ( rng f);

        consider x be object such that

         A10: x in the carrier of V & y = (f . x) by A9, FUNCT_2: 11;

        reconsider z = x as VECTOR of V by A10;

        per cases ;

          suppose not z in {v};

          then (f . z) = 0 by A6;

          hence y in INT by A10, NUMBERS: 17;

        end;

          suppose z in {v};

          then (f . z) = a0 by A4, TARSKI:def 1;

          hence y in INT by A10, INT_1:def 2;

        end;

      end;

      hence thesis by A8;

    end;

    theorem :: RLVECT_X:17

    v in ( Z_Lin {v})

    proof

      v in {v} by TARSKI:def 1;

      hence thesis by Th12;

    end;

    theorem :: RLVECT_X:18

    x in (v + ( Z_Lin {w})) iff ex a be Integer st x = (v + (a * w))

    proof

      thus x in (v + ( Z_Lin {w})) implies ex a be Integer st x = (v + (a * w))

      proof

        assume x in (v + ( Z_Lin {w}));

        then

        consider u be VECTOR of V such that

         A1: x = (v + u) and

         A2: u in ( Z_Lin {w});

        ex a be Integer st u = (a * w) by A2, Th16;

        hence thesis by A1;

      end;

      given a0 be Integer such that

       A3: x = (v + (a0 * w));

      (a0 * w) in ( Z_Lin {w}) by Th16;

      hence thesis by A3;

    end;

    theorem :: RLVECT_X:19

    

     Th19: x in ( Z_Lin {w1, w2}) iff ex a,b be Integer st x = ((a * w1) + (b * w2))

    proof

      thus x in ( Z_Lin {w1, w2}) implies ex a,b be Integer st x = ((a * w1) + (b * w2))

      proof

        assume

         A1: x in ( Z_Lin {w1, w2});

        now

          per cases ;

            suppose w1 = w2;

            then {w1, w2} = {w1} by ENUMSET1: 29;

            then

            consider a be Integer such that

             A2: x = (a * w1) by A1, Th16;

            consider b be Integer such that

             A3: b = 0 ;

            x = ((a * w1) + ( 0. V)) by A2, RLVECT_1: 4;

            then x = ((a * w1) + (b * w2)) by A3, RLVECT_1: 10;

            hence thesis;

          end;

            suppose

             A4: w1 <> w2;

            consider l be Linear_Combination of {w1, w2} such that

             A5: x = ( Sum l) & ( rng l) c= INT by A1;

            

             A6: x = (((l . w1) * w1) + ((l . w2) * w2)) by A4, A5, RLVECT_2: 33;

            ex f be Function st l = f & ( dom f) = the carrier of V & ( rng f) c= REAL by FUNCT_2:def 2;

            then (l . w1) in ( rng l) & (l . w2) in ( rng l) by FUNCT_1: 3;

            hence thesis by A5, A6;

          end;

        end;

        hence thesis;

      end;

      given a0,b0 be Integer such that

       A7: x = ((a0 * w1) + (b0 * w2));

      reconsider a = a0, b = b0 as Element of REAL by XREAL_0:def 1;

      now

        per cases ;

          suppose

           A8: w1 = w2;

          then x = ((a + b) * w1) by A7, RLVECT_1:def 6;

          then x in ( Z_Lin {w1}) by Th16;

          hence thesis by A8, ENUMSET1: 29;

        end;

          suppose

           A9: w1 <> w2;

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

           A10: (f . w1) = a & (f . w2) = b and

           A11: for u st u <> w1 & u <> w2 holds (f . u) = H(u) from FUNCT_2:sch 7( A9);

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

           A12:

          now

            let u;

            assume not u in {w1, w2};

            then u <> w1 & u <> w2 by TARSKI:def 2;

            hence (f . u) = 0 by A11;

          end;

          then

          reconsider f as Linear_Combination of V by RLVECT_2:def 3;

          ( Carrier f) c= {w1, w2}

          proof

            let x be object;

            assume that

             A13: x in ( Carrier f) and

             A14: not x in {w1, w2};

            x <> w1 & x <> w2 by A14, TARSKI:def 2;

            then (f . x) = 0 by A11, A13;

            hence contradiction by A13, RLVECT_2: 19;

          end;

          then

          reconsider f as Linear_Combination of {w1, w2} by RLVECT_2:def 6;

          

           A15: x = ( Sum f) by A7, A9, A10, RLVECT_2: 33;

          ( rng f) c= INT

          proof

            let y be object;

            assume

             A16: y in ( rng f);

            consider x be object such that

             A17: x in the carrier of V & y = (f . x) by A16, FUNCT_2: 11;

            reconsider v = x as VECTOR of V by A17;

            per cases ;

              suppose not v in {w1, w2};

              then (f . v) = 0 by A12;

              hence y in INT by A17, NUMBERS: 17;

            end;

              suppose v in {w1, w2};

              then (f . v) = a0 or (f . v) = b0 by A10, TARSKI:def 2;

              hence y in INT by A17, INT_1:def 2;

            end;

          end;

          hence thesis by A15;

        end;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_X:20

    w1 in ( Z_Lin {w1, w2})

    proof

      w1 in {w1, w2} by TARSKI:def 2;

      hence thesis by Th12;

    end;

    theorem :: RLVECT_X:21

    x in (v + ( Z_Lin {w1, w2})) iff ex a,b be Integer st x = ((v + (a * w1)) + (b * w2))

    proof

      thus x in (v + ( Z_Lin {w1, w2})) implies ex a,b be Integer st x = ((v + (a * w1)) + (b * w2))

      proof

        assume x in (v + ( Z_Lin {w1, w2}));

        then

        consider u such that

         A1: x = (v + u) and

         A2: u in ( Z_Lin {w1, w2});

        consider a,b be Integer such that

         A3: u = ((a * w1) + (b * w2)) by A2, Th19;

        take a, b;

        thus thesis by A1, A3, RLVECT_1:def 3;

      end;

      given a,b be Integer such that

       A4: x = ((v + (a * w1)) + (b * w2));

      ((a * w1) + (b * w2)) in ( Z_Lin {w1, w2}) by Th19;

      then (v + ((a * w1) + (b * w2))) in (v + ( Z_Lin {w1, w2}));

      hence thesis by A4, RLVECT_1:def 3;

    end;

    theorem :: RLVECT_X:22

    

     Th22: x in ( Z_Lin {v1, v2, v3}) iff ex a,b,c be Integer st x = (((a * v1) + (b * v2)) + (c * v3))

    proof

      thus x in ( Z_Lin {v1, v2, v3}) implies ex a,b,c be Integer st x = (((a * v1) + (b * v2)) + (c * v3))

      proof

        assume

         A1: x in ( Z_Lin {v1, v2, v3});

        now

          per cases ;

            suppose

             A2: v1 <> v2 & v1 <> v3 & v2 <> v3;

            consider l be Linear_Combination of {v1, v2, v3} such that

             A3: x = ( Sum l) & ( rng l) c= INT by A1;

            

             A4: x = ((((l . v1) * v1) + ((l . v2) * v2)) + ((l . v3) * v3)) by A2, A3, RLVECT_4: 6;

            ex f be Function st l = f & ( dom f) = the carrier of V & ( rng f) c= REAL by FUNCT_2:def 2;

            then (l . v1) in ( rng l) & (l . v2) in ( rng l) & (l . v3) in ( rng l) by FUNCT_1: 3;

            hence thesis by A3, A4;

          end;

            suppose v1 = v2 or v1 = v3 or v2 = v3;

            then

             A5: {v1, v2, v3} = {v1, v3} or {v1, v2, v3} = {v1, v1, v2} or {v1, v2, v3} = {v3, v3, v1} by ENUMSET1: 30, ENUMSET1: 59;

            now

              per cases by A5, ENUMSET1: 30;

                suppose {v1, v2, v3} = {v1, v2};

                then

                consider a,b be Integer such that

                 A6: x = ((a * v1) + (b * v2)) by A1, Th19;

                consider c be Integer such that

                 A7: c = 0 ;

                x = (((a * v1) + (b * v2)) + ( 0. V)) by A6, RLVECT_1: 4

                .= (((a * v1) + (b * v2)) + (c * v3)) by A7, RLVECT_1: 10;

                hence thesis;

              end;

                suppose {v1, v2, v3} = {v1, v3};

                then

                consider a,b be Integer such that

                 A8: x = ((a * v1) + (b * v3)) by A1, Th19;

                consider c be Integer such that

                 A9: c = 0 ;

                x = (((a * v1) + ( 0. V)) + (b * v3)) by A8, RLVECT_1: 4

                .= (((a * v1) + (c * v2)) + (b * v3)) by A9, RLVECT_1: 10;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      given a0,b0,c0 be Integer such that

       A10: x = (((a0 * v1) + (b0 * v2)) + (c0 * v3));

      reconsider a = a0, b = b0, c = c0 as Element of REAL by XREAL_0:def 1;

      now

        per cases ;

          suppose

           A11: v1 = v2 or v1 = v3 or v2 = v3;

          now

            per cases by A11;

              suppose v1 = v2;

              then {v1, v2, v3} = {v1, v3} & x = (((a + b) * v1) + (c * v3)) by A10, ENUMSET1: 30, RLVECT_1:def 6;

              hence thesis by Th19;

            end;

              suppose

               A12: v1 = v3;

              

              then

               A13: {v1, v2, v3} = {v1, v1, v2} by ENUMSET1: 57

              .= {v2, v1} by ENUMSET1: 30;

              x = ((b * v2) + ((a * v1) + (c * v1))) by A10, A12, RLVECT_1:def 3

              .= ((b * v2) + ((a + c) * v1)) by RLVECT_1:def 6;

              hence thesis by A13, Th19;

            end;

              suppose

               A14: v2 = v3;

              

              then

               A15: {v1, v2, v3} = {v2, v2, v1} by ENUMSET1: 59

              .= {v1, v2} by ENUMSET1: 30;

              x = ((a * v1) + ((b * v2) + (c * v2))) by A10, A14, RLVECT_1:def 3

              .= ((a * v1) + ((b + c) * v2)) by RLVECT_1:def 6;

              hence thesis by A15, Th19;

            end;

          end;

          hence thesis;

        end;

          suppose

           A16: v1 <> v2 & v1 <> v3 & v2 <> v3;

          

           A17: v1 <> v3 by A16;

          

           A18: v2 <> v3 by A16;

          

           A19: v1 <> v2 by A16;

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

           A20: (f . v1) = a & (f . v2) = b & (f . v3) = c and

           A21: for v st v <> v1 & v <> v2 & v <> v3 holds (f . v) = H(v) from RLVECT_4:sch 1( A19, A17, A18);

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

           A22:

          now

            let v;

            assume

             A23: not v in {v1, v2, v3};

            then

             A24: v <> v3 by ENUMSET1:def 1;

            v <> v1 & v <> v2 by A23, ENUMSET1:def 1;

            hence (f . v) = 0 by A21, A24;

          end;

          then

          reconsider f as Linear_Combination of V by RLVECT_2:def 3;

          ( Carrier f) c= {v1, v2, v3}

          proof

            let x be object;

            assume that

             A25: x in ( Carrier f) and

             A26: not x in {v1, v2, v3};

            

             A27: x <> v3 by A26, ENUMSET1:def 1;

            x <> v1 & x <> v2 by A26, ENUMSET1:def 1;

            then (f . x) = 0 by A21, A25, A27;

            hence thesis by A25, RLVECT_2: 19;

          end;

          then

          reconsider f as Linear_Combination of {v1, v2, v3} by RLVECT_2:def 6;

          

           A28: x = ( Sum f) by A10, A16, A20, RLVECT_4: 6;

          ( rng f) c= INT

          proof

            let y be object;

            assume

             A29: y in ( rng f);

            consider x be object such that

             A30: x in the carrier of V & y = (f . x) by A29, FUNCT_2: 11;

            reconsider v = x as VECTOR of V by A30;

            per cases ;

              suppose not v in {v1, v2, v3};

              then (f . v) = 0 by A22;

              hence y in INT by A30, NUMBERS: 17;

            end;

              suppose v in {v1, v2, v3};

              then (f . v) = a0 or (f . v) = b0 or (f . v) = c0 by A20, ENUMSET1:def 1;

              hence y in INT by A30, INT_1:def 2;

            end;

          end;

          hence thesis by A28;

        end;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_X:23

    w1 in ( Z_Lin {w1, w2, w3}) & w2 in ( Z_Lin {w1, w2, w3}) & w3 in ( Z_Lin {w1, w2, w3})

    proof

      

       A1: w3 in {w1, w2, w3} by ENUMSET1:def 1;

      w1 in {w1, w2, w3} & w2 in {w1, w2, w3} by ENUMSET1:def 1;

      hence thesis by A1, Th12;

    end;

    theorem :: RLVECT_X:24

    x in (v + ( Z_Lin {w1, w2, w3})) iff ex a,b,c be Integer st x = (((v + (a * w1)) + (b * w2)) + (c * w3))

    proof

      thus x in (v + ( Z_Lin {w1, w2, w3})) implies ex a,b,c be Integer st x = (((v + (a * w1)) + (b * w2)) + (c * w3))

      proof

        assume x in (v + ( Z_Lin {w1, w2, w3}));

        then

        consider u such that

         A1: x = (v + u) and

         A2: u in ( Z_Lin {w1, w2, w3});

        consider a,b,c be Integer such that

         A3: u = (((a * w1) + (b * w2)) + (c * w3)) by A2, Th22;

        take a, b, c;

        x = ((v + ((a * w1) + (b * w2))) + (c * w3)) by A1, A3, RLVECT_1:def 3;

        hence thesis by RLVECT_1:def 3;

      end;

      given a,b,c be Integer such that

       A4: x = (((v + (a * w1)) + (b * w2)) + (c * w3));

      (((a * w1) + (b * w2)) + (c * w3)) in ( Z_Lin {w1, w2, w3}) by Th22;

      then (v + (((a * w1) + (b * w2)) + (c * w3))) in (v + ( Z_Lin {w1, w2, w3}));

      then ((v + ((a * w1) + (b * w2))) + (c * w3)) in (v + ( Z_Lin {w1, w2, w3})) by RLVECT_1:def 3;

      hence thesis by A4, RLVECT_1:def 3;

    end;

    

     Lm1: for RS be RealLinearSpace, X be Subset of RS, g1,h1 be FinSequence of RS, a1 be INT -valued FinSequence st ( rng g1) c= X & ( len g1) = ( len h1) & ( len g1) = ( len a1) & for i be Nat st i in ( Seg ( len g1)) holds (h1 /. i) = ((a1 . i) * (g1 /. i)) holds ( Sum h1) in ( Z_Lin X)

    proof

      let RS be RealLinearSpace, X be Subset of RS;

      defpred P[ Nat] means for g,h be FinSequence of RS, s be INT -valued FinSequence st ( rng g) c= X & ( len g) = $1 & ( len g) = ( len h) & ( len g) = ( len s) & for i be Nat st i in ( Seg ( len g)) holds (h /. i) = ((s . i) * (g /. i)) holds ( Sum h) in ( Z_Lin X);

      

       A1: P[ 0 ]

      proof

        let g,h be FinSequence of RS, s be INT -valued FinSequence;

        set x = ( Sum h);

        assume

         A2: ( rng g) c= X & ( len g) = 0 & ( len g) = ( len h) & ( len g) = ( len s) & for i be Nat st i in ( Seg ( len g)) holds (h /. i) = ((s . i) * (g /. i));

        ( Sum h) = ( Sum ( <*> the carrier of RS)) by A2, FINSEQ_1: 20

        .= ( 0. RS) by RLVECT_1: 43;

        hence x in ( Z_Lin X) by Th11;

      end;

       A3:

      now

        let n be Nat;

        assume

         A4: P[n];

        now

          let g,h be FinSequence of RS, s be INT -valued FinSequence, x be set;

          assume

           A5: x = ( Sum h) & ( rng g) c= X & ( len g) = (n + 1) & ( len g) = ( len h) & ( len g) = ( len s) & for i be Nat st i in ( Seg ( len g)) holds (h /. i) = ((s . i) * (g /. i));

          reconsider gn = (g | n) as FinSequence of RS;

          reconsider hn = (h | n) as FinSequence of RS;

          reconsider sn = (s | n) as real-valued FinSequence;

          ( rng gn) c= X & ( len gn) = n & ( len gn) = ( len hn) & ( len gn) = ( len sn) & for i be Nat st i in ( Seg ( len gn)) holds (hn /. i) = ((sn . i) * (gn /. i))

          proof

            ( rng gn) c= ( rng g) by RELAT_1: 70;

            then

             A6: ( rng gn) c= X by A5;

            

             A7: n <= ( len g) by A5, NAT_1: 11;

            

             A8: n <= ( len h) by A5, NAT_1: 11;

            

             A9: ( len hn) = n by A5, FINSEQ_1: 59, NAT_1: 11;

            

             A10: ( len sn) = n by A5, FINSEQ_1: 59, NAT_1: 11;

            for i be Nat st i in ( Seg ( len gn)) holds (hn /. i) = ((sn . i) * (gn /. i))

            proof

              per cases ;

                suppose n = 0 ;

                hence thesis;

              end;

                suppose n <> 0 ;

                then

                 A11: n >= 1 by NAT_1: 14;

                let i be Nat;

                assume i in ( Seg ( len gn));

                then

                 A12: i in ( Seg n) by A5, FINSEQ_1: 59, NAT_1: 11;

                n in ( Seg ( len g)) by A7, A11;

                then n in ( dom g) by FINSEQ_1:def 3;

                then

                 A13: (gn /. i) = (g /. i) by A12, FINSEQ_4: 71;

                n in ( Seg ( len h)) by A8, A11;

                then n in ( dom h) by FINSEQ_1:def 3;

                then

                 A14: (hn /. i) = (h /. i) by A12, FINSEQ_4: 71;

                i <= n by A12, FINSEQ_1: 1;

                then (sn . i) = (s . i) by FINSEQ_3: 112;

                hence thesis by A5, A12, A13, A14, FINSEQ_2: 8;

              end;

            end;

            hence thesis by A6, A9, A10, A5, FINSEQ_1: 59, NAT_1: 11;

          end;

          then

           A15: ( Sum hn) in ( Z_Lin X) by A4;

          

           A16: (n + 1) in ( Seg ( len g)) by A5, FINSEQ_1: 4;

          

           A17: (h /. (n + 1)) = ((s . (n + 1)) * (g /. (n + 1))) by A5, FINSEQ_1: 4;

          

           A18: h = (hn ^ <*((s . (n + 1)) * (g /. (n + 1)))*>) by A5, A17, FINSEQ_5: 21;

          

           A19: (n + 1) in ( dom g) by A16, FINSEQ_1:def 3;

          then (g /. (n + 1)) = (g . (n + 1)) by PARTFUN1:def 6;

          then (g /. (n + 1)) in ( rng g) by A19, FUNCT_1: 3;

          then (g /. (n + 1)) in ( Z_Lin X) by A5, Th12;

          then

           A20: ((s . (n + 1)) * (g /. (n + 1))) in ( Z_Lin X) by Th10;

          ( Sum h) = (( Sum hn) + ( Sum <*((s . (n + 1)) * (g /. (n + 1)))*>)) by A18, RLVECT_1: 41

          .= (( Sum hn) + ((s . (n + 1)) * (g /. (n + 1)))) by RLVECT_1: 44;

          hence x in ( Z_Lin X) by A5, A15, A20, Th9;

        end;

        hence P[(n + 1)];

      end;

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

      hence thesis;

    end;

    

     Lm2: for x be set st x in ( Z_Lin A) holds ex g1,h1 be FinSequence of V, a1 be INT -valued FinSequence st x = ( Sum h1) & ( rng g1) c= A & ( len g1) = ( len h1) & ( len g1) = ( len a1) & for i be Nat st i in ( Seg ( len g1)) holds (h1 /. i) = ((a1 . i) * (g1 /. i))

    proof

      let x be set;

      assume x in ( Z_Lin A);

      then

      consider z be Linear_Combination of A such that

       A1: x = ( Sum z) & ( rng z) c= INT ;

      consider F be FinSequence of V such that

       A2: F is one-to-one & ( rng F) = ( Carrier z) & ( Sum z) = ( Sum (z (#) F)) by RLVECT_2:def 8;

      

       A3: ( len (z (#) F)) = ( len F) & for i be Nat st i in ( dom (z (#) F)) holds ((z (#) F) . i) = ((z . (F /. i)) * (F /. i)) by RLVECT_2:def 7;

      defpred P0[ Nat, set] means $2 = (z . (F /. $1));

       A4:

      now

        let k be Nat;

        assume k in ( Seg ( len F));

        (z . (F /. k)) in ( rng z) by FUNCT_2: 4;

        hence ex x be Element of INT st P0[k, x] by A1;

      end;

      consider u be FinSequence of INT such that

       A5: ( dom u) = ( Seg ( len F)) & for i be Nat st i in ( Seg ( len F)) holds P0[i, (u . i)] from FINSEQ_1:sch 5( A4);

      

       A6: ( rng F) c= A by A2, RLVECT_2:def 6;

      

       A7: ( len F) = ( len (z (#) F)) by RLVECT_2:def 7;

      

       A8: ( len F) = ( len u) by A5, FINSEQ_1:def 3;

      now

        let i be Nat;

        assume

         A9: i in ( Seg ( len F));

        then

         A10: i in ( dom (z (#) F)) by A3, FINSEQ_1:def 3;

        

        hence ((z (#) F) /. i) = ((z (#) F) . i) by PARTFUN1:def 6

        .= ((z . (F /. i)) * (F /. i)) by A10, RLVECT_2:def 7

        .= ((u . i) * (F /. i)) by A5, A9;

      end;

      hence thesis by A6, A7, A8, A1, A2;

    end;

    theorem :: RLVECT_X:25

    for x be set holds x in ( Z_Lin A) iff ex g1,h1 be FinSequence of V, a1 be INT -valued FinSequence st x = ( Sum h1) & ( rng g1) c= A & ( len g1) = ( len h1) & ( len g1) = ( len a1) & for i be Nat st i in ( Seg ( len g1)) holds (h1 /. i) = ((a1 . i) * (g1 /. i)) by Lm1, Lm2;

    registration

      let D be non empty set, n be Nat;

      cluster n -elementD -valued for FinSequence;

      existence

      proof

        take (n |-> the Element of D);

        thus thesis;

      end;

    end

    definition

      let RS be RealLinearSpace;

      let f be FinSequence of RS;

      :: RLVECT_X:def3

      func Z_Lin (f) -> Subset of RS equals { ( Sum g) where g be ( len f) -element FinSequence of RS : ex a be ( len f) -element INT -valued FinSequence st for i be Nat st i in ( Seg ( len f)) holds (g /. i) = ((a . i) * (f /. i)) };

      correctness

      proof

        now

          let x be object;

          assume x in { ( Sum g) where g be ( len f) -element FinSequence of RS : ex a be ( len f) -element INT -valued FinSequence st for i be Nat st i in ( Seg ( len f)) holds (g /. i) = ((a . i) * (f /. i)) };

          then ex g be ( len f) -element FinSequence of RS st x = ( Sum g) & ex a be ( len f) -element INT -valued FinSequence st for i be Nat st i in ( Seg ( len f)) holds (g /. i) = ((a . i) * (f /. i));

          hence x in the carrier of RS;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: RLVECT_X:26

    

     Th26: for RS be RealLinearSpace, f be FinSequence of RS, x be set holds x in ( Z_Lin f) iff ex g be ( len f) -element FinSequence of RS, a be ( len f) -element INT -valued FinSequence st x = ( Sum g) & for i be Nat st i in ( Seg ( len f)) holds (g /. i) = ((a . i) * (f /. i))

    proof

      let RS be RealLinearSpace, f be FinSequence of RS, x be set;

      hereby

        assume x in ( Z_Lin f);

        then

        consider g be ( len f) -element FinSequence of RS such that

         A1: x = ( Sum g) & ex s be ( len f) -element INT -valued FinSequence st for i be Nat st i in ( Seg ( len f)) holds (g /. i) = ((s . i) * (f /. i));

        consider s be ( len f) -element INT -valued FinSequence such that

         A2: for i be Nat st i in ( Seg ( len f)) holds (g /. i) = ((s . i) * (f /. i)) by A1;

        take g, s;

        thus x = ( Sum g) & for i be Nat st i in ( Seg ( len f)) holds (g /. i) = ((s . i) * (f /. i)) by A1, A2;

      end;

      assume ex g be ( len f) -element FinSequence of RS, a be ( len f) -element INT -valued FinSequence st x = ( Sum g) & for i be Nat st i in ( Seg ( len f)) holds (g /. i) = ((a . i) * (f /. i));

      hence x in ( Z_Lin f);

    end;

    theorem :: RLVECT_X:27

    

     Th27: for RS be RealLinearSpace, f be FinSequence of RS, x,y be Element of RS, a,b be Integer st x in ( Z_Lin f) & y in ( Z_Lin f) holds ((a * x) + (b * y)) in ( Z_Lin f)

    proof

      let RS be RealLinearSpace;

      let f be FinSequence of RS;

      let x,y be Element of RS;

      let a,b be Integer;

      assume

       A1: x in ( Z_Lin f) & y in ( Z_Lin f);

      consider g be ( len f) -element FinSequence of RS, s be ( len f) -element INT -valued FinSequence such that

       A2: x = ( Sum g) & for i be Nat st i in ( Seg ( len f)) holds (g /. i) = ((s . i) * (f /. i)) by A1, Th26;

      consider h be ( len f) -element FinSequence of RS, t be ( len f) -element INT -valued FinSequence such that

       A3: y = ( Sum h) & for i be Nat st i in ( Seg ( len f)) holds (h /. i) = ((t . i) * (f /. i)) by A1, Th26;

      defpred P0[ Nat, set] means $2 = ((a * (s . $1)) + (b * (t . $1)));

      

       A4: for k be Nat st k in ( Seg ( len f)) holds ex x be Element of INT st P0[k, x]

      proof

        let k be Nat;

        assume k in ( Seg ( len f));

        reconsider x = ((a * (s . k)) + (b * (t . k))) as Element of INT by INT_1:def 2;

        take x;

        thus P0[k, x];

      end;

      consider u be FinSequence of INT such that

       A5: ( dom u) = ( Seg ( len f)) & for i be Nat st i in ( Seg ( len f)) holds P0[i, (u . i)] from FINSEQ_1:sch 5( A4);

      ( len u) = ( len f) by A5, FINSEQ_1:def 3;

      then

      reconsider u as ( len f) -element INT -valued FinSequence by CARD_1:def 7;

      defpred P1[ Nat, set] means $2 = ((a * (g /. $1)) + (b * (h /. $1)));

      

       A6: for k be Nat st k in ( Seg ( len f)) holds ex x be Element of RS st P1[k, x];

      consider w be FinSequence of RS such that

       A7: ( dom w) = ( Seg ( len f)) & for i be Nat st i in ( Seg ( len f)) holds P1[i, (w . i)] from FINSEQ_1:sch 5( A6);

      ( len w) = ( len f) by A7, FINSEQ_1:def 3;

      then

      reconsider w as ( len f) -element FinSequence of RS by CARD_1:def 7;

       A8:

      now

        let i be Nat;

        assume

         A9: i in ( Seg ( len f));

        

        hence (w /. i) = (w . i) by A7, PARTFUN1:def 6

        .= ((a * (g /. i)) + (b * (h /. i))) by A7, A9;

      end;

      a in INT by INT_1:def 2;

      then

      reconsider a0 = a as Element of REAL by NUMBERS: 15;

      b in INT by INT_1:def 2;

      then

      reconsider b0 = b as Element of REAL by NUMBERS: 15;

      ( dom (a0 (#) g)) = ( dom g) by VFUNCT_1:def 4

      .= ( Seg ( len g)) by FINSEQ_1:def 3;

      then

       A10: (a0 (#) g) is FinSequence-like;

      ( rng (a0 (#) g)) c= the carrier of RS;

      then

      reconsider ag = (a0 (#) g) as FinSequence of RS by A10, FINSEQ_1:def 4;

      ( dom (b0 (#) h)) = ( dom h) by VFUNCT_1:def 4

      .= ( Seg ( len h)) by FINSEQ_1:def 3;

      then

       A11: (b0 (#) h) is FinSequence-like;

      ( rng (b0 (#) h)) c= the carrier of RS;

      then

      reconsider bh = (b0 (#) h) as FinSequence of RS by A11, FINSEQ_1:def 4;

      

       A12: ( dom (a0 (#) g)) = ( dom g) by VFUNCT_1:def 4

      .= ( Seg ( len g)) by FINSEQ_1:def 3

      .= ( Seg ( len f)) by CARD_1:def 7;

      then

       A13: ( len ag) = ( len f) by FINSEQ_1:def 3;

      

       A14: ( dom (b0 (#) h)) = ( dom h) by VFUNCT_1:def 4

      .= ( Seg ( len h)) by FINSEQ_1:def 3

      .= ( Seg ( len f)) by CARD_1:def 7;

       A15:

      now

        let i be Nat;

        assume

         A16: i in ( dom ag);

        

        hence (w . i) = ((a * (g /. i)) + (b * (h /. i))) by A7, A12

        .= ((ag /. i) + (b * (h /. i))) by A16, VFUNCT_1:def 4

        .= ((ag /. i) + (bh /. i)) by A16, A14, A12, VFUNCT_1:def 4;

      end;

      

       A17: ( len ag) = ( len bh) & ( len ag) = ( len w) by A7, A13, A14, FINSEQ_1:def 3;

      

       A18: for i be Nat st i in ( Seg ( len f)) holds (w /. i) = ((u . i) * (f /. i))

      proof

        let i be Nat;

        assume

         A19: i in ( Seg ( len f));

        

        hence (w /. i) = ((a * (g /. i)) + (b * (h /. i))) by A8

        .= ((a * ((s . i) * (f /. i))) + (b * (h /. i))) by A19, A2

        .= ((a * ((s . i) * (f /. i))) + (b * ((t . i) * (f /. i)))) by A19, A3

        .= (((a * (s . i)) * (f /. i)) + (b * ((t . i) * (f /. i)))) by RLVECT_1:def 7

        .= (((a * (s . i)) * (f /. i)) + ((b * (t . i)) * (f /. i))) by RLVECT_1:def 7

        .= (((a * (s . i)) + (b * (t . i))) * (f /. i)) by RLVECT_1:def 6

        .= ((u . i) * (f /. i)) by A19, A5;

      end;

      ((a * x) + (b * y)) = (( Sum ag) + (b * ( Sum h))) by A2, A3, Th3

      .= (( Sum ag) + ( Sum bh)) by Th3

      .= ( Sum w) by A15, A17, RLVECT_2: 2;

      hence ((a * x) + (b * y)) in ( Z_Lin f) by A18;

    end;

    theorem :: RLVECT_X:28

    

     Th28: for RS be RealLinearSpace, f be FinSequence of RS st f = (( Seg ( len f)) --> ( 0. RS)) holds ( Sum f) = ( 0. RS)

    proof

      let RS be RealLinearSpace, f be FinSequence of RS;

      assume

       A1: f = (( Seg ( len f)) --> ( 0. RS));

       A2:

      now

        let k be Nat, v be Element of RS;

        assume

         A3: k in ( dom f) & v = (f . k);

        then k in ( Seg ( len f)) by FINSEQ_1:def 3;

        then (f . k) = ( 0. RS) by A1, FUNCOP_1: 7;

        hence (f . k) = ( - v) by A3, RLVECT_1: 12;

      end;

      ( len f) = ( len f);

      then ( Sum f) = ( - ( Sum f)) by A2, RLVECT_1: 40;

      hence thesis by RLVECT_1: 19;

    end;

    theorem :: RLVECT_X:29

    

     Th29: for RS be RealLinearSpace, f be FinSequence of RS, v be Element of RS, i be Nat st i in ( Seg ( len f)) & f = ((( Seg ( len f)) --> ( 0. RS)) +* ( {i} --> v)) holds ( Sum f) = v

    proof

      let RS be RealLinearSpace, f be FinSequence of RS;

      let v be Element of RS, i be Nat;

      defpred P[ Nat] means for g be FinSequence of RS st ( len g) = $1 & i in ( Seg ( len g)) & g = ((( Seg ( len g)) --> ( 0. RS)) +* ( {i} --> v)) holds ( Sum g) = v;

      

       A1: P[ 0 ];

       A2:

      now

        let n be Nat;

        assume

         A3: P[n];

        now

          let f be FinSequence of RS;

          assume

           A4: ( len f) = (n + 1) & i in ( Seg ( len f)) & f = ((( Seg ( len f)) --> ( 0. RS)) +* ( {i} --> v));

          reconsider g = (f | n) as FinSequence of RS;

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

          then

           A5: (n + 1) in ( dom f) by A4, FINSEQ_1:def 3;

          

           A6: ( len g) = n by A4, FINSEQ_1: 59, NAT_1: 11;

          f = ((f | n) ^ <*(f . (n + 1))*>) by A4, FINSEQ_3: 55

          .= (g ^ <*(f /. (n + 1))*>) by A5, PARTFUN1:def 6;

          then

           A7: ( Sum f) = (( Sum g) + ( Sum <*(f /. (n + 1))*>)) by RLVECT_1: 41;

          

           A8: ( dom ( {i} --> v)) = {i} by FUNCOP_1: 13;

          let f1 be Function such that

           A9: f1 = (( Seg ( len f)) --> ( 0. RS));

          let f2 be Function such that

           A10: f2 = ( {i} --> v);

          per cases ;

            suppose

             A11: i = (n + 1);

            then ( dom f2) = {(n + 1)} by A10, FUNCOP_1: 13;

            

            then g = (f1 | ( Seg n)) by A4, A9, A10, FINSEQ_3: 14, FUNCT_4: 72

            .= ((( Seg ( len f)) /\ ( Seg n)) --> ( 0. RS)) by A9, FUNCOP_1: 12;

            then

             A12: g = (( Seg n) --> ( 0. RS)) by A4, FINSEQ_1: 7, NAT_1: 11;

            

             A13: (n + 1) in {(n + 1)} by ZFMISC_1: 31;

            then (n + 1) in ( dom f2) by A10, A11, FUNCOP_1: 13;

            

            then (f . (n + 1)) = (f2 . (n + 1)) by A4, A10, FUNCT_4: 13

            .= v by A10, A11, A13, FUNCOP_1: 7;

            then

             A14: (f /. (n + 1)) = v by A5, PARTFUN1:def 6;

            ( Sum g) = ( 0. RS) by A6, A12, Th28;

            

            hence ( Sum f) = (( 0. RS) + v) by A7, A14, RLVECT_1: 44

            .= v by RLVECT_1: 4;

          end;

            suppose

             A15: i <> (n + 1);

            then i < (n + 1) or i > (n + 1) by XXREAL_0: 1;

            then 1 <= i & i <= n by A4, FINSEQ_1: 1, NAT_1: 13;

            then

             A16: i in ( Seg ( len g)) by A6;

            g = ((f1 | ( Seg n)) +* (f2 | ( Seg n))) by A4, A9, A10, FUNCT_4: 71

            .= (((( Seg ( len f)) /\ ( Seg n)) --> ( 0. RS)) +* (f2 | ( Seg n))) by A9, FUNCOP_1: 12

            .= ((( Seg ( len g)) --> ( 0. RS)) +* (f2 | ( Seg n))) by A4, A6, FINSEQ_1: 7, NAT_1: 11

            .= ((( Seg ( len g)) --> ( 0. RS)) +* (( {i} /\ ( Seg n)) --> v)) by A10, FUNCOP_1: 12;

            then

             A17: g = ((( Seg ( len g)) --> ( 0. RS)) +* ( {i} --> v)) by A6, A16, ZFMISC_1: 46;

             not {(n + 1)} c= ( dom f2) by A8, A10, A15, ZFMISC_1: 3;

            then not (n + 1) in ( dom f2) by ZFMISC_1: 31;

            

            then (f . (n + 1)) = (f1 . (n + 1)) by A4, A9, A10, FUNCT_4: 11

            .= ( 0. RS) by A4, A9, FINSEQ_1: 4, FUNCOP_1: 7;

            then

             A18: (f /. (n + 1)) = ( 0. RS) by A5, PARTFUN1:def 6;

            ( Sum g) = v by A16, A17, A6, A3;

            

            hence ( Sum f) = (v + ( 0. RS)) by A7, A18, RLVECT_1: 44

            .= v by RLVECT_1: 4;

          end;

        end;

        hence P[(n + 1)];

      end;

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

      hence thesis;

    end;

    theorem :: RLVECT_X:30

    

     Th30: for RS be RealLinearSpace, f be FinSequence of RS, i be Nat st i in ( Seg ( len f)) holds (f /. i) in ( Z_Lin f)

    proof

      let RS be RealLinearSpace, f be FinSequence of RS;

      let i be Nat;

      assume

       A1: i in ( Seg ( len f));

      set s = ((( Seg ( len f)) --> 0 ) +* ( {i} --> 1));

      

       A2: ( dom s) = ( Seg ( len f))

      proof

        ( dom s) = (( dom (( Seg ( len f)) --> 0 )) \/ ( dom ( {i} --> 1))) by FUNCT_4:def 1

        .= (( Seg ( len f)) \/ ( dom ( {i} --> 1))) by FUNCOP_1: 13

        .= (( Seg ( len f)) \/ {i}) by FUNCOP_1: 13;

        hence thesis by A1, ZFMISC_1: 40;

      end;

      then

       A3: s is FinSequence-like;

      ( rng s) c= INT

      proof

        

         A4: ( rng s) c= (( rng (( Seg ( len f)) --> 0 )) \/ ( rng ( {i} --> 1))) by FUNCT_4: 17;

        ( Seg ( len f)) <> {} by A1;

        then

         A5: ( rng (( Seg ( len f)) --> 0 )) = { 0 } & ( rng ( {i} --> 1)) = {1} by FUNCOP_1: 8;

        1 in INT & 0 in INT by INT_1:def 2;

        then ( rng (( Seg ( len f)) --> 0 )) c= INT & ( rng ( {i} --> 1)) c= INT by A5, ZFMISC_1: 31;

        then (( rng (( Seg ( len f)) --> 0 )) \/ ( rng ( {i} --> 1))) c= INT by XBOOLE_1: 8;

        hence thesis by A4;

      end;

      then

      reconsider s as FinSequence of INT by A3, FINSEQ_1:def 4;

      ( len s) = ( len f) by A2, FINSEQ_1:def 3;

      then

      reconsider s as ( len f) -element INT -valued FinSequence by CARD_1:def 7;

      defpred Q[ Nat, set] means $2 = ((s . $1) * (f /. $1));

      

       A6: for k be Nat st k in ( Seg ( len f)) holds ex x be Element of RS st Q[k, x];

      consider w be FinSequence of RS such that

       A7: ( dom w) = ( Seg ( len f)) & for i be Nat st i in ( Seg ( len f)) holds Q[i, (w . i)] from FINSEQ_1:sch 5( A6);

      

       A8: ( len w) = ( len f) by A7, FINSEQ_1:def 3;

      then

      reconsider w as ( len f) -element FinSequence of RS by CARD_1:def 7;

      now

        let i be Nat;

        assume

         A9: i in ( Seg ( len f));

        

        hence (w /. i) = (w . i) by A7, PARTFUN1:def 6

        .= ((s . i) * (f /. i)) by A7, A9;

      end;

      then

       A10: ( Sum w) in ( Z_Lin f);

      

       A11: w = ((( Seg ( len w)) --> ( 0. RS)) +* ( {i} --> (f /. i)))

      proof

        consider w1 be Function such that

         A12: w1 = (( Seg ( len f)) --> ( 0. RS));

        

         A13: ( dom w1) = ( Seg ( len f)) by A12, FUNCOP_1: 13;

        consider w2 be Function such that

         A14: w2 = ( {i} --> (f /. i));

        

         A15: ( dom w2) = {i} by A14, FUNCOP_1: 13;

        consider ww be Function such that

         A16: ww = (w1 +* w2);

        

         A17: ( dom ww) = (( Seg ( len f)) \/ {i}) by A13, A15, A16, FUNCT_4:def 1

        .= ( Seg ( len f)) by A1, ZFMISC_1: 40;

        then

        reconsider ww as FinSequence by FINSEQ_1:def 2;

        ( rng w1) c= {( 0. RS)} by A12, FUNCOP_1: 13;

        then

         A18: ( rng w1) c= the carrier of RS by XBOOLE_1: 1;

        ( rng w2) c= {(f /. i)} by A14, FUNCOP_1: 13;

        then

         A19: ( rng w2) c= the carrier of RS by XBOOLE_1: 1;

        

         A20: ( rng ww) c= (( rng w1) \/ ( rng w2)) by A16, FUNCT_4: 17;

        (( rng w1) \/ ( rng w2)) c= the carrier of RS by A18, A19, XBOOLE_1: 8;

        then ( rng ww) c= the carrier of RS by A20;

        then

        reconsider ww as FinSequence of RS by FINSEQ_1:def 4;

        for j be Nat st j in ( dom w) holds (w /. j) = (ww /. j)

        proof

          let j be Nat such that

           A21: j in ( dom w);

          

           A22: ( dom ( {i} --> 1)) = {i} by FUNCOP_1: 13;

          per cases ;

            suppose

             A23: j in ( dom w2);

            then

             A24: j = i by A15, TARSKI:def 1;

            then (w /. j) = (w . i) by A21, PARTFUN1:def 6;

            then

             A25: (w /. j) = ((s . i) * (f /. i)) by A7, A21, A24;

            

             A26: i in {i} by TARSKI:def 1;

            

            then

             A27: (s . i) = (( {i} --> 1) . i) by A22, FUNCT_4: 13

            .= 1 by A26, FUNCOP_1: 7;

            (ww /. j) = (ww . j) by A7, A17, A21, PARTFUN1:def 6

            .= (w2 . j) by A16, A23, FUNCT_4: 13

            .= (f /. i) by A14, A15, A23, FUNCOP_1: 7;

            hence thesis by A25, A27, RLVECT_1:def 8;

          end;

            suppose

             A28: not j in ( dom w2);

            (w /. j) = (w . j) by A21, PARTFUN1:def 6;

            then

             A29: (w /. j) = ((s . j) * (f /. j)) by A7, A21;

             not j in ( dom ( {i} --> 1)) by A15, A28;

            

            then

             A30: (s . j) = ((( Seg ( len f)) --> 0 ) . j) by FUNCT_4: 11

            .= 0 by A7, A21, FUNCOP_1: 7;

            (ww /. j) = (ww . j) by A7, A17, A21, PARTFUN1:def 6

            .= (w1 . j) by A16, A28, FUNCT_4: 11

            .= ( 0. RS) by A7, A12, A21, FUNCOP_1: 7;

            hence thesis by A29, A30, RLVECT_1: 10;

          end;

        end;

        hence thesis by A7, A8, A12, A14, A16, A17, FINSEQ_5: 12;

      end;

      i in ( Seg ( len w)) by A7, A1, FINSEQ_1:def 3;

      hence (f /. i) in ( Z_Lin f) by A10, A11, Th29;

    end;

    theorem :: RLVECT_X:31

    

     Th31: for RS be RealLinearSpace, f be FinSequence of RS holds ( rng f) c= ( Z_Lin f)

    proof

      let RS be RealLinearSpace, f be FinSequence of RS;

      let y be object;

      assume y in ( rng f);

      then

      consider x be object such that

       A1: x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

      

       A2: x in ( Seg ( len f)) by A1, FINSEQ_1:def 3;

      reconsider i = x as Nat by A1;

      y = (f /. i) by A1, PARTFUN1:def 6;

      hence y in ( Z_Lin f) by A2, Th30;

    end;

    theorem :: RLVECT_X:32

    

     Th32: for RS be RealLinearSpace, f be non empty FinSequence of RS, g,h be FinSequence of RS, s be INT -valued FinSequence st ( rng g) c= ( Z_Lin f) & ( len g) = ( len s) & ( len g) = ( len h) & for i be Nat st i in ( Seg ( len g)) holds (h /. i) = ((s . i) * (g /. i)) holds ( Sum h) in ( Z_Lin f)

    proof

      let RS be RealLinearSpace, f be non empty FinSequence of RS;

      1 <= 1 & 1 <= ( len f) by FINSEQ_1: 20;

      then 1 in ( Seg ( len f));

      then

       A1: (f /. 1) in ( Z_Lin f) by Th30;

      reconsider z0 = 0 as Element of INT by NUMBERS: 17;

      reconsider z1 = 1 as Element of INT by NUMBERS: 17;

      ((z0 * (f /. 1)) + (z0 * (f /. 1))) in ( Z_Lin f) by Th27, A1;

      then ((z0 * (f /. 1)) + ( 0. RS)) in ( Z_Lin f) by RLVECT_1: 10;

      then

       A2: (( 0. RS) + ( 0. RS)) in ( Z_Lin f) by RLVECT_1: 10;

      defpred P[ Nat] means for g,h be FinSequence of RS, s be INT -valued FinSequence st ( rng g) c= ( Z_Lin f) & ( len g) = $1 & ( len g) = ( len s) & ( len g) = ( len h) & for i be Nat st i in ( Seg ( len g)) holds (h /. i) = ((s . i) * (g /. i)) holds ( Sum h) in ( Z_Lin f);

      

       A3: P[ 0 ]

      proof

        let g,h be FinSequence of RS, s be INT -valued FinSequence;

        assume

         A4: ( rng g) c= ( Z_Lin f) & ( len g) = 0 & ( len g) = ( len s) & ( len g) = ( len h) & for i be Nat st i in ( Seg ( len g)) holds (h /. i) = ((s . i) * (g /. i));

        ( Sum h) = ( Sum ( <*> the carrier of RS)) by A4, FINSEQ_1: 20

        .= ( 0. RS) by RLVECT_1: 43;

        hence ( Sum h) in ( Z_Lin f) by A2, RLVECT_1: 4;

      end;

       A5:

      now

        let n be Nat;

        assume

         A6: P[n];

        now

          let g,h be FinSequence of RS, s be INT -valued FinSequence;

          assume

           A7: ( rng g) c= ( Z_Lin f) & ( len g) = (n + 1) & ( len g) = ( len s) & ( len g) = ( len h) & for i be Nat st i in ( Seg ( len g)) holds (h /. i) = ((s . i) * (g /. i));

          reconsider gn = (g | n) as FinSequence of RS;

          reconsider hn = (h | n) as FinSequence of RS;

          reconsider sn = (s | n) as INT -valued FinSequence;

          

           A8: ( rng gn) c= ( Z_Lin f) & ( len gn) = n & ( len gn) = ( len sn) & ( len gn) = ( len hn) & for i be Nat st i in ( Seg ( len gn)) holds (hn /. i) = ((sn . i) * (gn /. i))

          proof

            

             A9: ( rng gn) c= ( rng g) by RELAT_1: 70;

            

             A10: n <= ( len g) by A7, NAT_1: 11;

            

             A11: n <= ( len h) by A7, NAT_1: 11;

            

             A12: ( len hn) = n by A7, FINSEQ_1: 59, NAT_1: 11;

            

             A13: ( len sn) = n by A7, FINSEQ_1: 59, NAT_1: 11;

            for i be Nat st i in ( Seg ( len gn)) holds (hn /. i) = ((sn . i) * (gn /. i))

            proof

              per cases ;

                suppose n = 0 ;

                hence thesis;

              end;

                suppose n <> 0 ;

                then

                 A14: n >= 1 by NAT_1: 14;

                let i be Nat;

                assume i in ( Seg ( len gn));

                then

                 A15: i in ( Seg n) by A7, FINSEQ_1: 59, NAT_1: 11;

                n in ( Seg ( len g)) by A10, A14;

                then n in ( dom g) by FINSEQ_1:def 3;

                then

                 A16: (gn /. i) = (g /. i) by A15, FINSEQ_4: 71;

                n in ( Seg ( len h)) by A11, A14;

                then n in ( dom h) by FINSEQ_1:def 3;

                then

                 A17: (hn /. i) = (h /. i) by A15, FINSEQ_4: 71;

                i <= n by A15, FINSEQ_1: 1;

                then (sn . i) = (s . i) by FINSEQ_3: 112;

                hence thesis by A7, A15, A16, A17, FINSEQ_2: 8;

              end;

            end;

            hence thesis by A9, A10, A12, A13, A7, FINSEQ_1: 59;

          end;

          

           A18: ( Sum hn) in ( Z_Lin f) by A8, A6;

          

           A19: (n + 1) in ( Seg ( len g)) by A7, FINSEQ_1: 4;

          

           A20: (h /. (n + 1)) = ((s . (n + 1)) * (g /. (n + 1))) by A7, FINSEQ_1: 4;

          

           A21: h = (hn ^ <*((s . (n + 1)) * (g /. (n + 1)))*>) by A7, A20, FINSEQ_5: 21;

          

           A22: (n + 1) in ( dom g) by A19, FINSEQ_1:def 3;

          then (g /. (n + 1)) = (g . (n + 1)) by PARTFUN1:def 6;

          then (g /. (n + 1)) in ( rng g) by A22, FUNCT_1: 3;

          then (((z1 * (s . (n + 1))) * (g /. (n + 1))) + (z0 * (g /. (n + 1)))) in ( Z_Lin f) by A7, Th27;

          then (((z1 * (s . (n + 1))) * (g /. (n + 1))) + ( 0. RS)) in ( Z_Lin f) by RLVECT_1: 10;

          then ((z1 * (s . (n + 1))) * (g /. (n + 1))) in ( Z_Lin f) by RLVECT_1: 4;

          then ((z1 * ( Sum hn)) + (z1 * ((s . (n + 1)) * (g /. (n + 1))))) in ( Z_Lin f) by A18, Th27;

          then

           A23: ((z1 * ( Sum hn)) + ((s . (n + 1)) * (g /. (n + 1)))) in ( Z_Lin f) by RLVECT_1:def 8;

          ( Sum h) = (( Sum hn) + ( Sum <*((s . (n + 1)) * (g /. (n + 1)))*>)) by A21, RLVECT_1: 41

          .= (( Sum hn) + ((s . (n + 1)) * (g /. (n + 1)))) by RLVECT_1: 44;

          hence ( Sum h) in ( Z_Lin f) by A23, RLVECT_1:def 8;

        end;

        hence P[(n + 1)];

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A3, A5);

      hence thesis;

    end;

    theorem :: RLVECT_X:33

    for RS be RealLinearSpace, f be non empty FinSequence of RS holds ( Z_Lin ( rng f)) = ( Z_Lin f)

    proof

      let RS be RealLinearSpace, f be non empty FinSequence of RS;

      for x be object holds x in ( Z_Lin ( rng f)) iff x in ( Z_Lin f)

      proof

        let x be object;

        hereby

          assume x in ( Z_Lin ( rng f));

          then

          consider g,h be FinSequence of RS, a be INT -valued FinSequence such that

           A1: x = ( Sum h) & ( rng g) c= ( rng f) & ( len g) = ( len h) & ( len g) = ( len a) & for i be Nat st i in ( Seg ( len g)) holds (h /. i) = ((a . i) * (g /. i)) by Lm2;

          ( rng f) c= ( Z_Lin f) by Th31;

          hence x in ( Z_Lin f) by A1, Th32, XBOOLE_1: 1;

        end;

        assume x in ( Z_Lin f);

        then

        consider g be ( len f) -element FinSequence of RS, a be ( len f) -element INT -valued FinSequence such that

         A2: x = ( Sum g) & for i be Nat st i in ( Seg ( len f)) holds (g /. i) = ((a . i) * (f /. i)) by Th26;

        ( len f) = ( len g) & ( len a) = ( len f) by CARD_1:def 7;

        hence x in ( Z_Lin ( rng f)) by A2, Lm1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RLVECT_X:34

    

     Th34: ( Lin ( Z_Lin A)) = ( Lin A)

    proof

      for x be object st x in A holds x in ( Z_Lin A) by Th12;

      then A c= ( Z_Lin A);

      then

       A1: ( Lin A) is Subspace of ( Lin ( Z_Lin A)) by RLVECT_3: 20;

      reconsider W = the carrier of ( Lin A) as Subset of V by RLSUB_1:def 2;

      ( Lin ( Z_Lin A)) is Subspace of ( Lin W) by Th8, RLVECT_3: 20;

      then ( Lin ( Z_Lin A)) is Subspace of ( Lin A) by RLVECT_3: 18;

      hence thesis by A1, RLSUB_1: 26;

    end;

    theorem :: RLVECT_X:35

    

     Th35: for x be set, g1,h1 be FinSequence of V, a1 be INT -valued FinSequence st x = ( Sum h1) & ( rng g1) c= ( Z_Lin A) & ( len g1) = ( len h1) & ( len g1) = ( len a1) & for i be Nat st i in ( Seg ( len g1)) holds (h1 /. i) = ((a1 . i) * (g1 /. i)) holds x in ( Z_Lin A)

    proof

      reconsider z0 = 0 as Element of INT by NUMBERS: 17;

      reconsider z1 = 1 as Element of INT by NUMBERS: 17;

      defpred P[ Nat] means for x be set, g1,h1 be FinSequence of V, a1 be INT -valued FinSequence st x = ( Sum h1) & ( rng g1) c= ( Z_Lin A) & ( len g1) = $1 & ( len g1) = ( len h1) & ( len g1) = ( len a1) & for i be Nat st i in ( Seg ( len g1)) holds (h1 /. i) = ((a1 . i) * (g1 /. i)) holds x in ( Z_Lin A);

      

       A1: P[ 0 ]

      proof

        let x be set, g1,h1 be FinSequence of V, a1 be INT -valued FinSequence;

        assume

         A2: x = ( Sum h1) & ( rng g1) c= ( Z_Lin A) & ( len g1) = 0 & ( len g1) = ( len h1) & ( len g1) = ( len a1) & for i be Nat st i in ( Seg ( len g1)) holds (h1 /. i) = ((a1 . i) * (g1 /. i));

        ( Sum h1) = ( Sum ( <*> the carrier of V)) by A2, FINSEQ_1: 20

        .= ( 0. V) by RLVECT_1: 43;

        hence x in ( Z_Lin A) by A2, Th11;

      end;

       A3:

      now

        let n be Nat;

        assume

         A4: P[n];

        now

          let x be set, g1,h1 be FinSequence of V, a1 be INT -valued FinSequence;

          assume

           A5: x = ( Sum h1) & ( rng g1) c= ( Z_Lin A) & ( len g1) = (n + 1) & ( len g1) = ( len h1) & ( len g1) = ( len a1) & for i be Nat st i in ( Seg ( len g1)) holds (h1 /. i) = ((a1 . i) * (g1 /. i));

          reconsider gn = (g1 | n) as FinSequence of V;

          reconsider hn = (h1 | n) as FinSequence of V;

          reconsider an = (a1 | n) as INT -valued FinSequence;

          

           A6: ( rng gn) c= ( Z_Lin A) & ( len gn) = n & ( len gn) = ( len an) & ( len gn) = ( len hn) & for i be Nat st i in ( Seg ( len gn)) holds (hn /. i) = ((an . i) * (gn /. i))

          proof

            

             A7: ( rng gn) c= ( rng g1) by RELAT_1: 70;

            

             A8: n <= ( len g1) by A5, NAT_1: 11;

            

             A9: n <= ( len h1) by A5, NAT_1: 11;

            

             A10: ( len hn) = n by A5, FINSEQ_1: 59, NAT_1: 11;

            

             A11: ( len an) = n by A5, FINSEQ_1: 59, NAT_1: 11;

            for i be Nat st i in ( Seg ( len gn)) holds (hn /. i) = ((an . i) * (gn /. i))

            proof

              per cases ;

                suppose n = 0 ;

                hence thesis;

              end;

                suppose n <> 0 ;

                then

                 A12: n >= 1 by NAT_1: 14;

                let i be Nat;

                assume i in ( Seg ( len gn));

                then

                 A13: i in ( Seg n) by A5, FINSEQ_1: 59, NAT_1: 11;

                n in ( Seg ( len g1)) by A8, A12;

                then n in ( dom g1) by FINSEQ_1:def 3;

                then

                 A14: (gn /. i) = (g1 /. i) by A13, FINSEQ_4: 71;

                n in ( Seg ( len h1)) by A9, A12;

                then n in ( dom h1) by FINSEQ_1:def 3;

                then

                 A15: (hn /. i) = (h1 /. i) by A13, FINSEQ_4: 71;

                i <= n by A13, FINSEQ_1: 1;

                then (an . i) = (a1 . i) by FINSEQ_3: 112;

                hence thesis by A5, A13, A14, A15, FINSEQ_2: 8;

              end;

            end;

            hence thesis by A5, A7, A8, A10, A11, FINSEQ_1: 59;

          end;

          

           A16: (n + 1) in ( Seg ( len g1)) by A5, FINSEQ_1: 4;

          

           A17: (h1 /. (n + 1)) = ((a1 . (n + 1)) * (g1 /. (n + 1))) by A5, FINSEQ_1: 4;

          

           A18: h1 = (hn ^ <*((a1 . (n + 1)) * (g1 /. (n + 1)))*>) by A5, A17, FINSEQ_5: 21;

          

           A19: (n + 1) in ( dom g1) by A16, FINSEQ_1:def 3;

          then (g1 /. (n + 1)) = (g1 . (n + 1)) by PARTFUN1:def 6;

          then (g1 /. (n + 1)) in ( rng g1) by A19, FUNCT_1: 3;

          then ((z1 * (a1 . (n + 1))) * (g1 /. (n + 1))) in ( Z_Lin A) & (z0 * (g1 /. (n + 1))) in ( Z_Lin A) by A5, Th10;

          then (((z1 * (a1 . (n + 1))) * (g1 /. (n + 1))) + (z0 * (g1 /. (n + 1)))) in ( Z_Lin A) by Th9;

          then (((z1 * (a1 . (n + 1))) * (g1 /. (n + 1))) + ( 0. V)) in ( Z_Lin A) by RLVECT_1: 10;

          then

           A20: ((z1 * (a1 . (n + 1))) * (g1 /. (n + 1))) in ( Z_Lin A) by RLVECT_1: 4;

          (z1 * ( Sum hn)) in ( Z_Lin A) by A4, A6, Th10;

          then

           A21: ((z1 * ( Sum hn)) + ((z1 * (a1 . (n + 1))) * (g1 /. (n + 1)))) in ( Z_Lin A) by A20, Th9;

          ( Sum h1) = (( Sum hn) + ( Sum <*((a1 . (n + 1)) * (g1 /. (n + 1)))*>)) by A18, RLVECT_1: 41

          .= (( Sum hn) + ((a1 . (n + 1)) * (g1 /. (n + 1)))) by RLVECT_1: 44;

          hence ( Sum h1) in ( Z_Lin A) by A21, RLVECT_1:def 8;

        end;

        hence P[(n + 1)];

      end;

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

      hence thesis;

    end;

    theorem :: RLVECT_X:36

    ( Z_Lin ( Z_Lin A)) = ( Z_Lin A)

    proof

      for x be object st x in A holds x in ( Z_Lin A) by Th12;

      then A c= ( Z_Lin A);

      then

       A1: ( Z_Lin A) c= ( Z_Lin ( Z_Lin A)) by Th13;

      ( Z_Lin ( Z_Lin A)) c= ( Z_Lin A)

      proof

        let x be object;

        assume x in ( Z_Lin ( Z_Lin A));

        then

        consider g1,h1 be FinSequence of V, a1 be INT -valued FinSequence such that

         A2: x = ( Sum h1) & ( rng g1) c= ( Z_Lin A) & ( len g1) = ( len h1) & ( len g1) = ( len a1) & for i be Nat st i in ( Seg ( len g1)) holds (h1 /. i) = ((a1 . i) * (g1 /. i)) by Lm2;

        thus x in ( Z_Lin A) by A2, Th35;

      end;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: RLVECT_X:37

    ( Z_Lin A) = ( Z_Lin B) implies ( Lin A) = ( Lin B)

    proof

      assume ( Z_Lin A) = ( Z_Lin B);

      

      hence ( Lin A) = ( Lin ( Z_Lin B)) by Th34

      .= ( Lin B) by Th34;

    end;