rlvect_3.miz



    begin

    reserve x,y for object,

X,Y,Z for set;

    reserve a,b for Real;

    reserve k for Element of NAT ;

    reserve V for RealLinearSpace;

    reserve W1,W2,W3 for Subspace of V;

    reserve v,v1,v2,u for VECTOR of V;

    reserve A,B,C for Subset of V;

    reserve T for finite Subset of V;

    reserve L,L1,L2 for Linear_Combination of V;

    reserve l for Linear_Combination of A;

    reserve F,G,H for FinSequence of the carrier of V;

    reserve f,g for Function of the carrier of V, REAL ;

    reserve p,q,r for FinSequence;

    reserve M for non empty set;

    reserve CF for Choice_Function of M;

    

     Lm1: (f (#) (F ^ G)) = ((f (#) F) ^ (f (#) G))

    proof

      set H = ((f (#) F) ^ (f (#) G));

      set I = (F ^ G);

      

       A1: ( len H) = (( len (f (#) F)) + ( len (f (#) G))) by FINSEQ_1: 22

      .= (( len F) + ( len (f (#) G))) by RLVECT_2:def 7

      .= (( len F) + ( len G)) by RLVECT_2:def 7

      .= ( len I) by FINSEQ_1: 22;

      

       A2: ( len F) = ( len (f (#) F)) by RLVECT_2:def 7;

      

       A3: ( len G) = ( len (f (#) G)) by RLVECT_2:def 7;

      now

        let k be Nat;

        assume

         A4: k in ( dom H);

        now

          per cases by A4, FINSEQ_1: 25;

            suppose

             A5: k in ( dom (f (#) F));

            then

             A6: k in ( dom F) by A2, FINSEQ_3: 29;

            then

             A7: k in ( dom (F ^ G)) by FINSEQ_3: 22;

            

             A8: (F /. k) = (F . k) by A6, PARTFUN1:def 6

            .= ((F ^ G) . k) by A6, FINSEQ_1:def 7

            .= ((F ^ G) /. k) by A7, PARTFUN1:def 6;

            

            thus (H . k) = ((f (#) F) . k) by A5, FINSEQ_1:def 7

            .= ((f . (I /. k)) * (I /. k)) by A5, A8, RLVECT_2:def 7;

          end;

            suppose

             A9: ex n be Nat st n in ( dom (f (#) G)) & k = (( len (f (#) F)) + n);

            

             A10: k in ( dom I) by A1, A4, FINSEQ_3: 29;

            consider n be Nat such that

             A11: n in ( dom (f (#) G)) and

             A12: k = (( len (f (#) F)) + n) by A9;

            

             A13: n in ( dom G) by A3, A11, FINSEQ_3: 29;

            

            then

             A14: (G /. n) = (G . n) by PARTFUN1:def 6

            .= ((F ^ G) . k) by A2, A12, A13, FINSEQ_1:def 7

            .= ((F ^ G) /. k) by A10, PARTFUN1:def 6;

            

            thus (H . k) = ((f (#) G) . n) by A11, A12, FINSEQ_1:def 7

            .= ((f . (I /. k)) * (I /. k)) by A11, A14, RLVECT_2:def 7;

          end;

        end;

        hence (H . k) = ((f . (I /. k)) * (I /. k));

      end;

      hence thesis by A1, RLVECT_2:def 7;

    end;

    theorem :: RLVECT_3:1

    

     Th1: ( Sum (L1 + L2)) = (( Sum L1) + ( Sum L2))

    proof

      consider F such that

       A1: F is one-to-one and

       A2: ( rng F) = ( Carrier (L1 + L2)) and

       A3: ( Sum ((L1 + L2) (#) F)) = ( Sum (L1 + L2)) by RLVECT_2:def 8;

      set A = ((( Carrier (L1 + L2)) \/ ( Carrier L1)) \/ ( Carrier L2));

      set C3 = (A \ ( Carrier (L1 + L2)));

      consider r such that

       A4: ( rng r) = C3 and

       A5: r is one-to-one by FINSEQ_4: 58;

      reconsider r as FinSequence of the carrier of V by A4, FINSEQ_1:def 4;

      set FF = (F ^ r);

      

       A6: A = (( Carrier (L1 + L2)) \/ (( Carrier L1) \/ ( Carrier L2))) by XBOOLE_1: 4;

      ( rng F) misses ( rng r)

      proof

        set x = the Element of (( rng F) /\ ( rng r));

        assume not thesis;

        then (( rng F) /\ ( rng r)) <> {} ;

        then x in ( Carrier (L1 + L2)) & x in C3 by A2, A4, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A7: FF is one-to-one by A1, A5, FINSEQ_3: 91;

      

       A8: ( len r) = ( len ((L1 + L2) (#) r)) by RLVECT_2:def 7;

      now

        let k be Nat;

        assume

         A9: k in ( dom r);

        then (r /. k) = (r . k) by PARTFUN1:def 6;

        then (r /. k) in C3 by A4, A9, FUNCT_1:def 3;

        then

         A10: not (r /. k) in ( Carrier (L1 + L2)) by XBOOLE_0:def 5;

        k in ( dom ((L1 + L2) (#) r)) by A8, A9, FINSEQ_3: 29;

        then (((L1 + L2) (#) r) . k) = (((L1 + L2) . (r /. k)) * (r /. k)) by RLVECT_2:def 7;

        hence (((L1 + L2) (#) r) . k) = ( 0 * (r /. k)) by A10;

      end;

      

      then

       A11: ( Sum ((L1 + L2) (#) r)) = ( 0 * ( Sum r)) by A8, RLVECT_2: 3

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

      set f = ((L1 + L2) (#) FF);

      set C1 = (A \ ( Carrier L1));

      consider G such that

       A12: G is one-to-one and

       A13: ( rng G) = ( Carrier L1) and

       A14: ( Sum (L1 (#) G)) = ( Sum L1) by RLVECT_2:def 8;

      consider p such that

       A15: ( rng p) = C1 and

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

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

      set GG = (G ^ p);

      

       A17: ( Sum f) = ( Sum (((L1 + L2) (#) F) ^ ((L1 + L2) (#) r))) by Lm1

      .= (( Sum ((L1 + L2) (#) F)) + ( 0. V)) by A11, RLVECT_1: 41

      .= ( Sum ((L1 + L2) (#) F));

      set C2 = (A \ ( Carrier L2));

      consider H such that

       A18: H is one-to-one and

       A19: ( rng H) = ( Carrier L2) and

       A20: ( Sum (L2 (#) H)) = ( Sum L2) by RLVECT_2:def 8;

      consider q such that

       A21: ( rng q) = C2 and

       A22: q is one-to-one by FINSEQ_4: 58;

      reconsider q as FinSequence of the carrier of V by A21, FINSEQ_1:def 4;

      set HH = (H ^ q);

      ( rng H) misses ( rng q)

      proof

        set x = the Element of (( rng H) /\ ( rng q));

        assume not thesis;

        then (( rng H) /\ ( rng q)) <> {} ;

        then x in ( Carrier L2) & x in C2 by A19, A21, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A23: HH is one-to-one by A18, A22, FINSEQ_3: 91;

      set h = (L2 (#) HH);

      

       A24: A = (( Carrier L1) \/ (( Carrier (L1 + L2)) \/ ( Carrier L2))) by XBOOLE_1: 4;

      ( rng GG) = (( rng G) \/ ( rng p)) by FINSEQ_1: 31;

      then ( rng GG) = (( Carrier L1) \/ A) by A13, A15, XBOOLE_1: 39;

      then

       A25: ( rng GG) = A by A24, XBOOLE_1: 7, XBOOLE_1: 12;

      

       A26: ( len q) = ( len (L2 (#) q)) by RLVECT_2:def 7;

      now

        let k be Nat;

        assume

         A27: k in ( dom q);

        then (q /. k) = (q . k) by PARTFUN1:def 6;

        then (q /. k) in C2 by A21, A27, FUNCT_1:def 3;

        then

         A28: not (q /. k) in ( Carrier L2) by XBOOLE_0:def 5;

        k in ( dom (L2 (#) q)) by A26, A27, FINSEQ_3: 29;

        then ((L2 (#) q) . k) = ((L2 . (q /. k)) * (q /. k)) by RLVECT_2:def 7;

        hence ((L2 (#) q) . k) = ( 0 * (q /. k)) by A28;

      end;

      

      then

       A29: ( Sum (L2 (#) q)) = ( 0 * ( Sum q)) by A26, RLVECT_2: 3

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

      

       A30: ( Sum h) = ( Sum ((L2 (#) H) ^ (L2 (#) q))) by Lm1

      .= (( Sum (L2 (#) H)) + ( 0. V)) by A29, RLVECT_1: 41

      .= ( Sum (L2 (#) H));

      deffunc Q( Nat) = (FF <- (GG . $1));

      set g = (L1 (#) GG);

      consider P be FinSequence such that

       A31: ( len P) = ( len FF) and

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

      

       A33: ( dom P) = ( Seg ( len FF)) by A31, FINSEQ_1:def 3;

      

       A34: ( len p) = ( len (L1 (#) p)) by RLVECT_2:def 7;

      now

        let k be Nat;

        assume

         A35: k in ( dom p);

        then (p /. k) = (p . k) by PARTFUN1:def 6;

        then (p /. k) in C1 by A15, A35, FUNCT_1:def 3;

        then

         A36: not (p /. k) in ( Carrier L1) by XBOOLE_0:def 5;

        k in ( dom (L1 (#) p)) by A34, A35, FINSEQ_3: 29;

        then ((L1 (#) p) . k) = ((L1 . (p /. k)) * (p /. k)) by RLVECT_2:def 7;

        hence ((L1 (#) p) . k) = ( 0 * (p /. k)) by A36;

      end;

      

      then

       A37: ( Sum (L1 (#) p)) = ( 0 * ( Sum p)) by A34, RLVECT_2: 3

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

      

       A38: ( Sum g) = ( Sum ((L1 (#) G) ^ (L1 (#) p))) by Lm1

      .= (( Sum (L1 (#) G)) + ( 0. V)) by A37, RLVECT_1: 41

      .= ( Sum (L1 (#) G));

      ( rng FF) = (( rng F) \/ ( rng r)) by FINSEQ_1: 31;

      then ( rng FF) = (( Carrier (L1 + L2)) \/ A) by A2, A4, XBOOLE_1: 39;

      then

       A39: ( rng FF) = A by A6, XBOOLE_1: 7, XBOOLE_1: 12;

      ( rng G) misses ( rng p)

      proof

        set x = the Element of (( rng G) /\ ( rng p));

        assume not thesis;

        then (( rng G) /\ ( rng p)) <> {} ;

        then x in ( Carrier L1) & x in C1 by A13, A15, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A40: GG is one-to-one by A12, A16, FINSEQ_3: 91;

      then

       A41: ( len GG) = ( len FF) by A7, A25, A39, FINSEQ_1: 48;

      

       A42: ( dom P) = ( Seg ( len FF)) by A31, FINSEQ_1:def 3;

       A43:

      now

        let x be object;

        assume

         A44: x in ( dom GG);

        then

        reconsider n = x as Element of NAT by FINSEQ_3: 23;

        (GG . n) in ( rng FF) by A25, A39, A44, FUNCT_1:def 3;

        then

         A45: FF just_once_values (GG . n) by A7, FINSEQ_4: 8;

        n in ( Seg ( len FF)) by A41, A44, FINSEQ_1:def 3;

        

        then (FF . (P . n)) = (FF . (FF <- (GG . n))) by A32, A42

        .= (GG . n) by A45, FINSEQ_4:def 3;

        hence (GG . x) = (FF . (P . x));

      end;

      

       A46: ( rng P) c= ( Seg ( len FF))

      proof

        let x be object;

        assume x in ( rng P);

        then

        consider y be object such that

         A47: y in ( dom P) and

         A48: (P . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A47, FINSEQ_3: 23;

        y in ( Seg ( len FF)) by A31, A47, FINSEQ_1:def 3;

        then y in ( dom GG) by A41, FINSEQ_1:def 3;

        then (GG . y) in ( rng FF) by A25, A39, FUNCT_1:def 3;

        then

         A49: FF just_once_values (GG . y) by A7, FINSEQ_4: 8;

        (P . y) = (FF <- (GG . y)) by A32, A47;

        then (P . y) in ( dom FF) by A49, FINSEQ_4:def 3;

        hence thesis by A48, FINSEQ_1:def 3;

      end;

      now

        let x be object;

        thus x in ( dom GG) implies x in ( dom P) & (P . x) in ( dom FF)

        proof

          assume x in ( dom GG);

          then x in ( Seg ( len P)) by A41, A31, FINSEQ_1:def 3;

          hence x in ( dom P) by FINSEQ_1:def 3;

          then (P . x) in ( rng P) by FUNCT_1:def 3;

          then (P . x) in ( Seg ( len FF)) by A46;

          hence thesis by FINSEQ_1:def 3;

        end;

        assume that

         A50: x in ( dom P) and (P . x) in ( dom FF);

        x in ( Seg ( len P)) by A50, FINSEQ_1:def 3;

        hence x in ( dom GG) by A41, A31, FINSEQ_1:def 3;

      end;

      then

       A51: GG = (FF * P) by A43, FUNCT_1: 10;

      ( Seg ( len FF)) c= ( rng P)

      proof

        set f = ((FF " ) * GG);

        let x be object;

        assume

         A52: x in ( Seg ( len FF));

        ( dom (FF " )) = ( rng GG) by A7, A25, A39, FUNCT_1: 33;

        

        then

         A53: ( rng f) = ( rng (FF " )) by RELAT_1: 28

        .= ( dom FF) by A7, FUNCT_1: 33;

        

         A54: ( rng P) c= ( dom FF) by A46, FINSEQ_1:def 3;

        f = (((FF " ) * FF) * P) by A51, RELAT_1: 36

        .= (( id ( dom FF)) * P) by A7, FUNCT_1: 39

        .= P by A54, RELAT_1: 53;

        hence thesis by A52, A53, FINSEQ_1:def 3;

      end;

      then

       A55: ( Seg ( len FF)) = ( rng P) by A46;

      then

       A56: P is one-to-one by A33, FINSEQ_4: 60;

      reconsider P as Function of ( Seg ( len FF)), ( Seg ( len FF)) by A46, A33, FUNCT_2: 2;

      reconsider P as Permutation of ( Seg ( len FF)) by A55, A56, FUNCT_2: 57;

      

       A57: ( len f) = ( len FF) by RLVECT_2:def 7;

      then

       A58: ( Seg ( len FF)) = ( dom f) by FINSEQ_1:def 3;

      then

      reconsider Fp = (f * P) as FinSequence of the carrier of V by FINSEQ_2: 47;

      

       A59: ( len g) = ( len GG) by RLVECT_2:def 7;

      deffunc Q( Nat) = (HH <- (GG . $1));

      consider R be FinSequence such that

       A60: ( len R) = ( len HH) and

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

      

       A62: ( dom R) = ( Seg ( len HH)) by A60, FINSEQ_1:def 3;

      ( rng HH) = (( rng H) \/ ( rng q)) by FINSEQ_1: 31;

      then ( rng HH) = (( Carrier L2) \/ A) by A19, A21, XBOOLE_1: 39;

      then

       A63: ( rng HH) = A by XBOOLE_1: 7, XBOOLE_1: 12;

      then

       A64: ( len GG) = ( len HH) by A23, A40, A25, FINSEQ_1: 48;

      

       A65: ( dom R) = ( Seg ( len HH)) by A60, FINSEQ_1:def 3;

       A66:

      now

        let x be object;

        assume

         A67: x in ( dom GG);

        then

        reconsider n = x as Element of NAT by FINSEQ_3: 23;

        (GG . n) in ( rng HH) by A25, A63, A67, FUNCT_1:def 3;

        then

         A68: HH just_once_values (GG . n) by A23, FINSEQ_4: 8;

        n in ( Seg ( len HH)) by A64, A67, FINSEQ_1:def 3;

        

        then (HH . (R . n)) = (HH . (HH <- (GG . n))) by A61, A65

        .= (GG . n) by A68, FINSEQ_4:def 3;

        hence (GG . x) = (HH . (R . x));

      end;

      

       A69: ( rng R) c= ( Seg ( len HH))

      proof

        let x be object;

        assume x in ( rng R);

        then

        consider y be object such that

         A70: y in ( dom R) and

         A71: (R . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A70, FINSEQ_3: 23;

        y in ( Seg ( len HH)) by A60, A70, FINSEQ_1:def 3;

        then y in ( dom GG) by A64, FINSEQ_1:def 3;

        then (GG . y) in ( rng HH) by A25, A63, FUNCT_1:def 3;

        then

         A72: HH just_once_values (GG . y) by A23, FINSEQ_4: 8;

        (R . y) = (HH <- (GG . y)) by A61, A70;

        then (R . y) in ( dom HH) by A72, FINSEQ_4:def 3;

        hence thesis by A71, FINSEQ_1:def 3;

      end;

      now

        let x be object;

        thus x in ( dom GG) implies x in ( dom R) & (R . x) in ( dom HH)

        proof

          assume x in ( dom GG);

          then x in ( Seg ( len R)) by A64, A60, FINSEQ_1:def 3;

          hence x in ( dom R) by FINSEQ_1:def 3;

          then (R . x) in ( rng R) by FUNCT_1:def 3;

          then (R . x) in ( Seg ( len HH)) by A69;

          hence thesis by FINSEQ_1:def 3;

        end;

        assume that

         A73: x in ( dom R) and (R . x) in ( dom HH);

        x in ( Seg ( len R)) by A73, FINSEQ_1:def 3;

        hence x in ( dom GG) by A64, A60, FINSEQ_1:def 3;

      end;

      then

       A74: GG = (HH * R) by A66, FUNCT_1: 10;

      ( Seg ( len HH)) c= ( rng R)

      proof

        set f = ((HH " ) * GG);

        let x be object;

        assume

         A75: x in ( Seg ( len HH));

        ( dom (HH " )) = ( rng GG) by A23, A25, A63, FUNCT_1: 33;

        

        then

         A76: ( rng f) = ( rng (HH " )) by RELAT_1: 28

        .= ( dom HH) by A23, FUNCT_1: 33;

        

         A77: ( rng R) c= ( dom HH) by A69, FINSEQ_1:def 3;

        f = (((HH " ) * HH) * R) by A74, RELAT_1: 36

        .= (( id ( dom HH)) * R) by A23, FUNCT_1: 39

        .= R by A77, RELAT_1: 53;

        hence thesis by A75, A76, FINSEQ_1:def 3;

      end;

      then

       A78: ( Seg ( len HH)) = ( rng R) by A69;

      then

       A79: R is one-to-one by A62, FINSEQ_4: 60;

      reconsider R as Function of ( Seg ( len HH)), ( Seg ( len HH)) by A69, A62, FUNCT_2: 2;

      reconsider R as Permutation of ( Seg ( len HH)) by A78, A79, FUNCT_2: 57;

      

       A80: ( len h) = ( len HH) by RLVECT_2:def 7;

      then

       A81: ( Seg ( len HH)) = ( dom h) by FINSEQ_1:def 3;

      then

      reconsider Hp = (h * R) as FinSequence of the carrier of V by FINSEQ_2: 47;

      

       A82: ( len Hp) = ( len GG) by A64, A80, A81, FINSEQ_2: 44;

      deffunc Q( Nat) = ((g /. $1) + (Hp /. $1));

      consider I be FinSequence such that

       A83: ( len I) = ( len GG) and

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

      ( dom I) = ( Seg ( len GG)) by A83, FINSEQ_1:def 3;

      then

       A85: for k be Nat st k in ( Seg ( len GG)) holds (I . k) = Q(k) by A84;

      ( rng I) c= the carrier of V

      proof

        let x be object;

        assume x in ( rng I);

        then

        consider y be object such that

         A86: y in ( dom I) and

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

        reconsider y as Element of NAT by A86, FINSEQ_3: 23;

        (I . y) = ((g /. y) + (Hp /. y)) by A84, A86;

        hence thesis by A87;

      end;

      then

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

      

       A88: ( len Fp) = ( len I) by A41, A57, A58, A83, FINSEQ_2: 44;

       A89:

      now

        let x be object;

        assume

         A90: x in ( dom I);

        then

        reconsider k = x as Element of NAT by FINSEQ_3: 23;

        

         A91: x in ( dom Hp) by A83, A82, A90, FINSEQ_3: 29;

        k in ( dom R) by A64, A62, A83, A90, FINSEQ_1:def 3;

        then

         A92: (R . k) in ( dom R) by A78, A62, FUNCT_1:def 3;

        then

        reconsider j = (R . k) as Element of NAT by FINSEQ_3: 23;

        set v = (GG /. k);

        

         A93: (R . k) in ( dom HH) by A60, A92, FINSEQ_3: 29;

        

         A94: x in ( dom GG) by A83, A90, FINSEQ_3: 29;

        

        then (HH . j) = (GG . k) by A66

        .= (GG /. k) by A94, PARTFUN1:def 6;

        then

         A95: (h . j) = ((L2 . v) * v) by A93, RLVECT_2: 24;

        k in ( dom P) by A41, A33, A83, A90, FINSEQ_1:def 3;

        then

         A96: (P . k) in ( dom P) by A55, A33, FUNCT_1:def 3;

        then

        reconsider l = (P . k) as Element of NAT by FINSEQ_3: 23;

        

         A97: (P . k) in ( dom FF) by A31, A96, FINSEQ_3: 29;

        x in ( dom Fp) by A88, A90, FINSEQ_3: 29;

        then

         A98: (Fp . k) = (f . (P . k)) by FUNCT_1: 12;

        k in ( dom Hp) by A83, A82, A90, FINSEQ_3: 29;

        

        then

         A99: (Hp /. k) = ((h * R) . k) by PARTFUN1:def 6

        .= (h . (R . k)) by A91, FUNCT_1: 12;

        

         A100: x in ( dom g) by A83, A59, A90, FINSEQ_3: 29;

        (FF . l) = (GG . k) by A43, A94

        .= (GG /. k) by A94, PARTFUN1:def 6;

        

        then

         A101: (f . l) = (((L1 + L2) . v) * v) by A97, RLVECT_2: 24

        .= (((L1 . v) + (L2 . v)) * v) by RLVECT_2:def 10

        .= (((L1 . v) * v) + ((L2 . v) * v)) by RLVECT_1:def 6;

        k in ( dom g) by A83, A59, A90, FINSEQ_3: 29;

        

        then (g /. k) = (g . k) by PARTFUN1:def 6

        .= ((L1 . v) * v) by A100, RLVECT_2:def 7;

        hence (I . x) = (Fp . x) by A84, A90, A99, A95, A98, A101;

      end;

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

      then

       A102: ( Sum Hp) = ( Sum h) by A80, RLVECT_2: 7;

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

      then

       A103: ( Sum Fp) = ( Sum f) by A57, RLVECT_2: 7;

      ( dom I) = ( Seg ( len I)) & ( dom Fp) = ( Seg ( len I)) by A88, FINSEQ_1:def 3;

      then

       A104: I = Fp by A89, FUNCT_1: 2;

      ( Seg ( len GG)) = ( dom g) by A59, FINSEQ_1:def 3;

      hence thesis by A3, A14, A20, A38, A30, A17, A103, A102, A83, A85, A82, A59, A104, RLVECT_2: 2;

    end;

    theorem :: RLVECT_3:2

    

     Th2: ( Sum (a * L)) = (a * ( Sum L))

    proof

      per cases ;

        suppose

         A1: a <> 0 ;

        set l = (a * L);

        consider F such that

         A2: F is one-to-one and

         A3: ( rng F) = ( Carrier (a * L)) and

         A4: ( Sum (a * L)) = ( Sum ((a * L) (#) F)) by RLVECT_2:def 8;

        set f = ((a * L) (#) F);

        consider G such that

         A5: G is one-to-one and

         A6: ( rng G) = ( Carrier L) and

         A7: ( Sum L) = ( Sum (L (#) G)) by RLVECT_2:def 8;

        

         A8: ( len G) = ( len F) by A1, A2, A3, A5, A6, FINSEQ_1: 48, RLVECT_2: 42;

        deffunc Q( Nat) = (F <- (G . $1));

        consider P be FinSequence such that

         A9: ( len P) = ( len F) and

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

        

         A11: ( Carrier l) = ( Carrier L) by A1, RLVECT_2: 42;

        

         A12: ( rng P) c= ( Seg ( len F))

        proof

          let x be object;

          assume x in ( rng P);

          then

          consider y be object such that

           A13: y in ( dom P) and

           A14: (P . y) = x by FUNCT_1:def 3;

          reconsider y as Element of NAT by A13, FINSEQ_3: 23;

          y in ( Seg ( len F)) by A9, A13, FINSEQ_1:def 3;

          then y in ( dom G) by A8, FINSEQ_1:def 3;

          then (G . y) in ( rng F) by A3, A6, A11, FUNCT_1:def 3;

          then

           A15: F just_once_values (G . y) by A2, FINSEQ_4: 8;

          (P . y) = (F <- (G . y)) by A10, A13;

          then (P . y) in ( dom F) by A15, FINSEQ_4:def 3;

          hence thesis by A14, FINSEQ_1:def 3;

        end;

         A16:

        now

          let x be object;

          thus x in ( dom G) implies x in ( dom P) & (P . x) in ( dom F)

          proof

            assume x in ( dom G);

            then x in ( Seg ( len P)) by A9, A8, FINSEQ_1:def 3;

            hence x in ( dom P) by FINSEQ_1:def 3;

            then (P . x) in ( rng P) by FUNCT_1:def 3;

            then (P . x) in ( Seg ( len F)) by A12;

            hence thesis by FINSEQ_1:def 3;

          end;

          assume that

           A17: x in ( dom P) and (P . x) in ( dom F);

          x in ( Seg ( len P)) by A17, FINSEQ_1:def 3;

          hence x in ( dom G) by A9, A8, FINSEQ_1:def 3;

        end;

        

         A18: ( dom P) = ( Seg ( len F)) by A9, FINSEQ_1:def 3;

        now

          let x be object;

          assume

           A19: x in ( dom G);

          then

          reconsider n = x as Element of NAT by FINSEQ_3: 23;

          (G . n) in ( rng F) by A3, A6, A11, A19, FUNCT_1:def 3;

          then

           A20: F just_once_values (G . n) by A2, FINSEQ_4: 8;

          n in ( Seg ( len F)) by A8, A19, FINSEQ_1:def 3;

          

          then (F . (P . n)) = (F . (F <- (G . n))) by A10, A18

          .= (G . n) by A20, FINSEQ_4:def 3;

          hence (G . x) = (F . (P . x));

        end;

        then

         A21: G = (F * P) by A16, FUNCT_1: 10;

        ( Seg ( len F)) c= ( rng P)

        proof

          set f = ((F " ) * G);

          let x be object;

          assume

           A22: x in ( Seg ( len F));

          ( dom (F " )) = ( rng G) by A2, A3, A6, A11, FUNCT_1: 33;

          

          then

           A23: ( rng f) = ( rng (F " )) by RELAT_1: 28

          .= ( dom F) by A2, FUNCT_1: 33;

          

           A24: ( rng P) c= ( dom F) by A12, FINSEQ_1:def 3;

          f = (((F " ) * F) * P) by A21, RELAT_1: 36

          .= (( id ( dom F)) * P) by A2, FUNCT_1: 39

          .= P by A24, RELAT_1: 53;

          hence thesis by A22, A23, FINSEQ_1:def 3;

        end;

        then

         A25: ( Seg ( len F)) = ( rng P) by A12;

        

         A26: ( dom P) = ( Seg ( len F)) by A9, FINSEQ_1:def 3;

        then

         A27: P is one-to-one by A25, FINSEQ_4: 60;

        reconsider P as Function of ( Seg ( len F)), ( Seg ( len F)) by A12, A26, FUNCT_2: 2;

        reconsider P as Permutation of ( Seg ( len F)) by A25, A27, FUNCT_2: 57;

        

         A28: ( len f) = ( len F) by RLVECT_2:def 7;

        then

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

        then

        reconsider Fp = (f * P) as FinSequence of the carrier of V by FINSEQ_2: 47;

        set g = (L (#) G);

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

        then

         A30: ( Sum Fp) = ( Sum f) by A28, RLVECT_2: 7;

        

         A31: ( len Fp) = ( len f) by A29, FINSEQ_2: 44;

        then

         A32: ( len Fp) = ( len g) by A8, A28, RLVECT_2:def 7;

         A33:

        now

          let k be Nat, v;

          assume that

           A34: k in ( dom g) and

           A35: v = (g . k);

          

           A36: k in ( Seg ( len F)) by A28, A31, A32, A34, FINSEQ_1:def 3;

          

           A37: k in ( dom G) by A8, A28, A31, A32, A34, FINSEQ_3: 29;

          then (G . k) in ( rng G) by FUNCT_1:def 3;

          then F just_once_values (G . k) by A2, A3, A6, A11, FINSEQ_4: 8;

          then

           A38: (F <- (G . k)) in ( dom F) by FINSEQ_4:def 3;

          then

          reconsider i = (F <- (G . k)) as Element of NAT by FINSEQ_3: 23;

          i in ( Seg ( len f)) by A28, A38, FINSEQ_1:def 3;

          then

           A39: i in ( dom f) by FINSEQ_1:def 3;

          

           A40: k in ( dom P) by A9, A28, A31, A32, A34, FINSEQ_3: 29;

          

           A41: (G /. k) = (G . k) by A37, PARTFUN1:def 6

          .= (F . (P . k)) by A21, A40, FUNCT_1: 13

          .= (F . i) by A10, A18, A36

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

          

          thus (Fp . k) = (f . (P . k)) by A40, FUNCT_1: 13

          .= (f . (F <- (G . k))) by A10, A18, A36

          .= ((l . (F /. i)) * (F /. i)) by A39, RLVECT_2:def 7

          .= ((a * (L . (F /. i))) * (F /. i)) by RLVECT_2:def 11

          .= (a * ((L . (F /. i)) * (F /. i))) by RLVECT_1:def 7

          .= (a * v) by A34, A35, A41, RLVECT_2:def 7;

        end;

        ( dom Fp) = ( dom g) by A32, FINSEQ_3: 29;

        hence thesis by A4, A7, A30, A32, A33, RLVECT_1: 39;

      end;

        suppose

         A42: a = 0 ;

        

        hence ( Sum (a * L)) = ( Sum ( ZeroLC V)) by RLVECT_2: 43

        .= ( 0. V) by RLVECT_2: 30

        .= (a * ( Sum L)) by A42, RLVECT_1: 10;

      end;

    end;

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

    theorem :: RLVECT_3:3

    

     Th3: ( Sum ( - L)) = ( - ( Sum L))

    proof

      

      thus ( Sum ( - L)) = (( - jj) * ( Sum L)) by Th2

      .= ( - ( Sum L)) by RLVECT_1: 16;

    end;

    theorem :: RLVECT_3:4

    

     Th4: ( Sum (L1 - L2)) = (( Sum L1) - ( Sum L2))

    proof

      

      thus ( Sum (L1 - L2)) = (( Sum L1) + ( Sum ( - L2))) by Th1

      .= (( Sum L1) + ( - ( Sum L2))) by Th3

      .= (( Sum L1) - ( Sum L2)) by RLVECT_1:def 11;

    end;

    definition

      let V;

      let A;

      :: RLVECT_3:def1

      attr A is linearly-independent means for l st ( Sum l) = ( 0. V) holds ( Carrier l) = {} ;

    end

    notation

      let V;

      let A;

      antonym A is linearly-dependent for A is linearly-independent;

    end

    theorem :: RLVECT_3:5

    A c= B & B is linearly-independent implies A is linearly-independent

    proof

      assume that

       A1: A c= B and

       A2: B is linearly-independent;

      let l be Linear_Combination of A;

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

      assume ( Sum l) = ( 0. V);

      then ( Carrier L) = {} by A2;

      hence thesis;

    end;

    theorem :: RLVECT_3:6

    

     Th6: A is linearly-independent implies not ( 0. V) in A

    proof

      assume that

       A1: A is linearly-independent and

       A2: ( 0. V) in A;

      deffunc F( Element of V) = ( In ( 0 , REAL ));

      consider f such that

       A3: (f . ( 0. V)) = jj and

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

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

      ex T st for v st not v in T holds (f . v) = 0

      proof

        take T = {( 0. V)};

        let v;

        assume not v in T;

        then v <> ( 0. V) by TARSKI:def 1;

        hence thesis by A4;

      end;

      then

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

      

       A5: ( Carrier f) = {( 0. V)}

      proof

        thus ( Carrier f) c= {( 0. V)}

        proof

          let x be object;

          assume x in ( Carrier f);

          then

          consider v such that

           A6: v = x and

           A7: (f . v) <> 0 ;

          v = ( 0. V) by A4, A7;

          hence thesis by A6, TARSKI:def 1;

        end;

        let x be object;

        assume x in {( 0. V)};

        then x = ( 0. V) by TARSKI:def 1;

        hence thesis by A3;

      end;

      then ( Carrier f) c= A by A2, ZFMISC_1: 31;

      then

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

      ( Sum f) = ((f . ( 0. V)) * ( 0. V)) by A5, RLVECT_2: 35

      .= ( 0. V);

      hence contradiction by A1, A5;

    end;

    theorem :: RLVECT_3:7

    

     Th7: ( {} the carrier of V) is linearly-independent

    proof

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

      ( Carrier l) c= {} by RLVECT_2:def 6;

      hence thesis;

    end;

    registration

      let V;

      cluster linearly-independent for Subset of V;

      existence

      proof

        take ( {} the carrier of V);

        thus thesis by Th7;

      end;

    end

    theorem :: RLVECT_3:8

    

     Th8: {v} is linearly-independent iff v <> ( 0. V)

    proof

      thus {v} is linearly-independent implies v <> ( 0. V)

      proof

        assume {v} is linearly-independent;

        then not ( 0. V) in {v} by Th6;

        hence thesis by TARSKI:def 1;

      end;

      assume

       A1: v <> ( 0. V);

      let l be Linear_Combination of {v};

      

       A2: ( Carrier l) c= {v} by RLVECT_2:def 6;

      assume

       A3: ( Sum l) = ( 0. V);

      now

        per cases by A2, ZFMISC_1: 33;

          suppose ( Carrier l) = {} ;

          hence thesis;

        end;

          suppose

           A4: ( Carrier l) = {v};

          

           A5: ( 0. V) = ((l . v) * v) by A3, RLVECT_2: 32;

          now

            assume v in ( Carrier l);

            then ex u st v = u & (l . u) <> 0 ;

            hence contradiction by A1, A5, RLVECT_1: 11;

          end;

          hence thesis by A4, TARSKI:def 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_3:9

     {( 0. V)} is linearly-dependent by Th8;

    theorem :: RLVECT_3:10

    

     Th10: {v1, v2} is linearly-independent implies v1 <> ( 0. V) & v2 <> ( 0. V)

    proof

      

       A1: v1 in {v1, v2} & v2 in {v1, v2} by TARSKI:def 2;

      assume {v1, v2} is linearly-independent;

      hence thesis by A1, Th6;

    end;

    theorem :: RLVECT_3:11

     {v, ( 0. V)} is linearly-dependent & {( 0. V), v} is linearly-dependent by Th10;

    theorem :: RLVECT_3:12

    

     Th12: v1 <> v2 & {v1, v2} is linearly-independent iff v2 <> ( 0. V) & for a holds v1 <> (a * v2)

    proof

      thus v1 <> v2 & {v1, v2} is linearly-independent implies v2 <> ( 0. V) & for a holds v1 <> (a * v2)

      proof

        deffunc F( Element of V) = ( In ( 0 , REAL ));

        assume that

         A1: v1 <> v2 and

         A2: {v1, v2} is linearly-independent;

        thus v2 <> ( 0. V) by A2, Th10;

        let a;

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

        consider f such that

         A3: (f . v1) = ( - jj) & (f . v2) = aa and

         A4: for v be Element of V st v <> v1 & v <> v2 holds (f . v) = F(v) from FUNCT_2:sch 7( A1);

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

        now

          let v;

          assume not v in {v1, v2};

          then v <> v1 & v <> v2 by TARSKI:def 2;

          hence (f . v) = 0 by A4;

        end;

        then

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

        ( Carrier f) c= {v1, v2}

        proof

          let x be object;

          assume x in ( Carrier f);

          then

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

          assume not x in {v1, v2};

          then x <> v1 & x <> v2 by TARSKI:def 2;

          hence thesis by A4, A5;

        end;

        then

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

        

         A6: v1 in ( Carrier f) by A3;

        set w = (a * v2);

        assume v1 = (a * v2);

        

        then ( Sum f) = ((( - jj) * w) + w) by A1, A3, RLVECT_2: 33

        .= (( - w) + w) by RLVECT_1: 16

        .= ( - (w - w)) by RLVECT_1: 33

        .= ( - ( 0. V)) by RLVECT_1: 15

        .= ( 0. V);

        hence thesis by A2, A6;

      end;

      assume

       A7: v2 <> ( 0. V);

      assume

       A8: for a holds v1 <> (a * v2);

      

       A9: (1 * v2) = v2 by RLVECT_1:def 8;

      hence v1 <> v2 by A8;

      let l be Linear_Combination of {v1, v2};

      assume that

       A10: ( Sum l) = ( 0. V) and

       A11: ( Carrier l) <> {} ;

      

       A12: ( 0. V) = (((l . v1) * v1) + ((l . v2) * v2)) by A8, A9, A10, RLVECT_2: 33;

      set x = the Element of ( Carrier l);

      ( Carrier l) c= {v1, v2} by RLVECT_2:def 6;

      then

       A13: x in {v1, v2} by A11;

      x in ( Carrier l) by A11;

      then

       A14: ex u st x = u & (l . u) <> 0 ;

      now

        per cases by A14, A13, TARSKI:def 2;

          suppose

           A15: (l . v1) <> 0 ;

          ( 0. V) = (((l . v1) " ) * (((l . v1) * v1) + ((l . v2) * v2))) by A12

          .= ((((l . v1) " ) * ((l . v1) * v1)) + (((l . v1) " ) * ((l . v2) * v2))) by RLVECT_1:def 5

          .= (((((l . v1) " ) * (l . v1)) * v1) + (((l . v1) " ) * ((l . v2) * v2))) by RLVECT_1:def 7

          .= (((((l . v1) " ) * (l . v1)) * v1) + ((((l . v1) " ) * (l . v2)) * v2)) by RLVECT_1:def 7

          .= ((1 * v1) + ((((l . v1) " ) * (l . v2)) * v2)) by A15, XCMPLX_0:def 7

          .= (v1 + ((((l . v1) " ) * (l . v2)) * v2)) by RLVECT_1:def 8;

          

          then v1 = ( - ((((l . v1) " ) * (l . v2)) * v2)) by RLVECT_1: 6

          .= (( - jj) * ((((l . v1) " ) * (l . v2)) * v2)) by RLVECT_1: 16

          .= ((( - jj) * (((l . v1) " ) * (l . v2))) * v2) by RLVECT_1:def 7;

          hence thesis by A8;

        end;

          suppose

           A16: (l . v2) <> 0 & (l . v1) = 0 ;

          ( 0. V) = (((l . v2) " ) * (((l . v1) * v1) + ((l . v2) * v2))) by A12

          .= ((((l . v2) " ) * ((l . v1) * v1)) + (((l . v2) " ) * ((l . v2) * v2))) by RLVECT_1:def 5

          .= (((((l . v2) " ) * (l . v1)) * v1) + (((l . v2) " ) * ((l . v2) * v2))) by RLVECT_1:def 7

          .= (((((l . v2) " ) * (l . v1)) * v1) + ((((l . v2) " ) * (l . v2)) * v2)) by RLVECT_1:def 7

          .= (((((l . v2) " ) * (l . v1)) * v1) + (1 * v2)) by A16, XCMPLX_0:def 7

          .= (( 0 * v1) + v2) by A16, RLVECT_1:def 8

          .= (( 0. V) + v2) by RLVECT_1: 10

          .= v2;

          hence thesis by A7;

        end;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_3:13

    v1 <> v2 & {v1, v2} is linearly-independent iff for a, b st ((a * v1) + (b * v2)) = ( 0. V) holds a = 0 & b = 0

    proof

      thus v1 <> v2 & {v1, v2} is linearly-independent implies for a, b st ((a * v1) + (b * v2)) = ( 0. V) holds a = 0 & b = 0

      proof

        assume

         A1: v1 <> v2 & {v1, v2} is linearly-independent;

        let a, b;

        assume that

         A2: ((a * v1) + (b * v2)) = ( 0. V) and

         A3: a <> 0 or b <> 0 ;

        now

          per cases by A3;

            suppose

             A4: a <> 0 ;

            ( 0. V) = ((a " ) * ((a * v1) + (b * v2))) by A2

            .= (((a " ) * (a * v1)) + ((a " ) * (b * v2))) by RLVECT_1:def 5

            .= ((((a " ) * a) * v1) + ((a " ) * (b * v2))) by RLVECT_1:def 7

            .= ((((a " ) * a) * v1) + (((a " ) * b) * v2)) by RLVECT_1:def 7

            .= ((1 * v1) + (((a " ) * b) * v2)) by A4, XCMPLX_0:def 7

            .= (v1 + (((a " ) * b) * v2)) by RLVECT_1:def 8;

            

            then v1 = ( - (((a " ) * b) * v2)) by RLVECT_1: 6

            .= (( - 1) * (((a " ) * b) * v2)) by RLVECT_1: 16

            .= ((( - 1) * ((a " ) * b)) * v2) by RLVECT_1:def 7;

            hence thesis by A1, Th12;

          end;

            suppose

             A5: b <> 0 ;

            ( 0. V) = ((b " ) * ((a * v1) + (b * v2))) by A2

            .= (((b " ) * (a * v1)) + ((b " ) * (b * v2))) by RLVECT_1:def 5

            .= ((((b " ) * a) * v1) + ((b " ) * (b * v2))) by RLVECT_1:def 7

            .= ((((b " ) * a) * v1) + (((b " ) * b) * v2)) by RLVECT_1:def 7

            .= ((((b " ) * a) * v1) + (1 * v2)) by A5, XCMPLX_0:def 7

            .= ((((b " ) * a) * v1) + v2) by RLVECT_1:def 8;

            

            then v2 = ( - (((b " ) * a) * v1)) by RLVECT_1:def 10

            .= (( - 1) * (((b " ) * a) * v1)) by RLVECT_1: 16

            .= ((( - 1) * ((b " ) * a)) * v1) by RLVECT_1:def 7;

            hence thesis by A1, Th12;

          end;

        end;

        hence thesis;

      end;

      assume

       A6: for a, b st ((a * v1) + (b * v2)) = ( 0. V) holds a = 0 & b = 0 ;

       A7:

      now

        let a;

        assume v1 = (a * v2);

        then v1 = (( 0. V) + (a * v2));

        

        then ( 0. V) = (v1 - (a * v2)) by RLSUB_2: 61

        .= (v1 + ( - (a * v2))) by RLVECT_1:def 11

        .= (v1 + (a * ( - v2))) by RLVECT_1: 25

        .= (v1 + (( - a) * v2)) by RLVECT_1: 24

        .= ((1 * v1) + (( - a) * v2)) by RLVECT_1:def 8;

        hence contradiction by A6;

      end;

      now

        assume

         A8: v2 = ( 0. V);

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

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

        .= (( 0 * v1) + (1 * v2)) by A8;

        hence contradiction by A6;

      end;

      hence thesis by A7, Th12;

    end;

    definition

      let V;

      let A;

      :: RLVECT_3:def2

      func Lin (A) -> strict Subspace of V means

      : Def2: the carrier of it = the set of all ( Sum l);

      existence

      proof

        set A1 = the set of all ( Sum l);

        A1 c= the carrier of V

        proof

          let x be object;

          assume x in A1;

          then ex l st x = ( Sum l);

          hence thesis;

        end;

        then

        reconsider A1 as Subset of V;

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

        

         A1: A1 is linearly-closed

        proof

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

          proof

            let v, u;

            assume that

             A2: v in A1 and

             A3: u in A1;

            consider l1 be Linear_Combination of A such that

             A4: v = ( Sum l1) by A2;

            consider l2 be Linear_Combination of A such that

             A5: u = ( Sum l2) by A3;

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

            (v + u) = ( Sum f) by A4, A5, Th1;

            hence thesis;

          end;

          let a be Real, v;

          assume v in A1;

          then

          consider l such that

           A6: v = ( Sum l);

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

          (a * v) = ( Sum f) by A6, Th2;

          hence thesis;

        end;

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

        then ( 0. V) in A1;

        hence thesis by A1, RLSUB_1: 35;

      end;

      uniqueness by RLSUB_1: 30;

    end

    theorem :: RLVECT_3:14

    

     Th14: x in ( Lin A) iff ex l st x = ( Sum l)

    proof

      thus x in ( Lin A) implies ex l st x = ( Sum l)

      proof

        assume x in ( Lin A);

        then x in the carrier of ( Lin A) by STRUCT_0:def 5;

        then x in the set of all ( Sum l) by Def2;

        hence thesis;

      end;

      given k be Linear_Combination of A such that

       A1: x = ( Sum k);

      x in the set of all ( Sum l) by A1;

      then x in the carrier of ( Lin A) by Def2;

      hence thesis by STRUCT_0:def 5;

    end;

    theorem :: RLVECT_3:15

    

     Th15: x in A implies x in ( Lin A)

    proof

      deffunc F( Element of V) = ( In ( 0 , REAL ));

      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) = jj and

       A3: for u 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;

      ex T 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) = (1 * v) by A2, RLVECT_2: 32

      .= v by 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;

      ( Sum f) = v by A7;

      hence thesis by Th14;

    end;

    

     Lm2: x in ( (0). V) iff x = ( 0. V)

    proof

      thus x in ( (0). V) implies x = ( 0. V)

      proof

        assume x in ( (0). V);

        then x in the carrier of ( (0). V) by STRUCT_0:def 5;

        then x in {( 0. V)} by RLSUB_1:def 3;

        hence thesis by TARSKI:def 1;

      end;

      thus thesis by RLSUB_1: 17;

    end;

    reserve l0 for Linear_Combination of ( {} the carrier of V);

    theorem :: RLVECT_3:16

    ( Lin ( {} the carrier of V)) = ( (0). V)

    proof

      set A = ( Lin ( {} the carrier of V));

      now

        let v;

        thus v in A implies v in ( (0). V)

        proof

          assume v in A;

          then

           A1: v in the carrier of A by STRUCT_0:def 5;

          the carrier of A = the set of all ( Sum l0) by Def2;

          then ex l0 st v = ( Sum l0) by A1;

          then v = ( 0. V) by RLVECT_2: 31;

          hence thesis by Lm2;

        end;

        assume v in ( (0). V);

        then v = ( 0. V) by Lm2;

        hence v in A by RLSUB_1: 17;

      end;

      hence thesis by RLSUB_1: 31;

    end;

    theorem :: RLVECT_3:17

    ( Lin A) = ( (0). V) implies A = {} or A = {( 0. V)}

    proof

      assume that

       A1: ( Lin A) = ( (0). V) and

       A2: A <> {} ;

      thus A c= {( 0. V)}

      proof

        let x be object;

        assume x in A;

        then x in ( Lin A) by Th15;

        then x = ( 0. V) by A1, Lm2;

        hence thesis by TARSKI:def 1;

      end;

      set y = the Element of A;

      let x be object;

      assume x in {( 0. V)};

      then

       A3: x = ( 0. V) by TARSKI:def 1;

      y in A & y in ( Lin A) by A2, Th15;

      hence thesis by A1, A3, Lm2;

    end;

    theorem :: RLVECT_3:18

    

     Th18: for W be strict Subspace of V holds A = the carrier of W implies ( Lin A) = W

    proof

      let W be strict Subspace of V;

      assume

       A1: A = the carrier of W;

      now

        let v;

        thus v in ( Lin A) implies v in W

        proof

          assume v in ( Lin A);

          then

           A2: ex l st v = ( Sum l) by Th14;

          A is linearly-closed by A1, RLSUB_1: 34;

          then v in the carrier of W by A1, A2, RLVECT_2: 29;

          hence thesis by STRUCT_0:def 5;

        end;

        v in W iff v in the carrier of W by STRUCT_0:def 5;

        hence v in W implies v in ( Lin A) by A1, Th15;

      end;

      hence thesis by RLSUB_1: 31;

    end;

    theorem :: RLVECT_3:19

    for V be strict RealLinearSpace, A be Subset of V holds A = the carrier of V implies ( Lin A) = V

    proof

      let V be strict RealLinearSpace, A be Subset of V;

      assume A = the carrier of V;

      then A = the carrier of ( (Omega). V);

      hence thesis by Th18;

    end;

    

     Lm3: W1 is Subspace of W3 implies (W1 /\ W2) is Subspace of W3

    proof

      

       A1: (W1 /\ W2) is Subspace of W1 by RLSUB_2: 16;

      assume W1 is Subspace of W3;

      hence thesis by A1, RLSUB_1: 27;

    end;

    

     Lm4: W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of (W2 /\ W3)

    proof

      assume

       A1: W1 is Subspace of W2 & W1 is Subspace of W3;

      now

        let v;

        assume v in W1;

        then v in W2 & v in W3 by A1, RLSUB_1: 8;

        hence v in (W2 /\ W3) by RLSUB_2: 3;

      end;

      hence thesis by RLSUB_1: 29;

    end;

    

     Lm5: W1 is Subspace of W2 implies W1 is Subspace of (W2 + W3)

    proof

      

       A1: W2 is Subspace of (W2 + W3) by RLSUB_2: 7;

      assume W1 is Subspace of W2;

      hence thesis by A1, RLSUB_1: 27;

    end;

    

     Lm6: W1 is Subspace of W3 & W2 is Subspace of W3 implies (W1 + W2) is Subspace of W3

    proof

      assume

       A1: W1 is Subspace of W3 & W2 is Subspace of W3;

      now

        let v;

        assume v in (W1 + W2);

        then

        consider v1, v2 such that

         A2: v1 in W1 & v2 in W2 and

         A3: v = (v1 + v2) by RLSUB_2: 1;

        v1 in W3 & v2 in W3 by A1, A2, RLSUB_1: 8;

        hence v in W3 by A3, RLSUB_1: 20;

      end;

      hence thesis by RLSUB_1: 29;

    end;

    theorem :: RLVECT_3:20

    

     Th20: A c= B implies ( Lin A) is Subspace of ( Lin B)

    proof

      assume

       A1: A c= B;

      now

        let v;

        assume v in ( Lin A);

        then

        consider l such that

         A2: v = ( Sum l) by Th14;

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

        ( Sum l) = v by A2;

        hence v in ( Lin B) by Th14;

      end;

      hence thesis by RLSUB_1: 29;

    end;

    theorem :: RLVECT_3:21

    for V be strict RealLinearSpace, A,B be Subset of V holds ( Lin A) = V & A c= B implies ( Lin B) = V

    proof

      let V be strict RealLinearSpace, A,B be Subset of V;

      assume ( Lin A) = V & A c= B;

      then V is Subspace of ( Lin B) by Th20;

      hence thesis by RLSUB_1: 26;

    end;

    theorem :: RLVECT_3:22

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

    proof

      now

        deffunc G( object) = 0 ;

        let v;

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

        then

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

         A1: v = ( Sum l) by Th14;

        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;

        now

          let x;

          assume x in the carrier of V;

          then

          reconsider v = x as VECTOR of V;

          (f . v) in REAL ;

          hence x in C implies (l . x) in REAL ;

          assume not x in C;

          thus 0 in REAL by XREAL_0:def 1;

        end;

        then

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

        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) = G(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: ( Carrier f) c= C

        proof

          let x be object;

          assume x in ( Carrier f);

          then

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

          assume not x in C;

          hence thesis by A3, A5;

        end;

        C c= A by XBOOLE_1: 17;

        then ( Carrier f) c= A by A4;

        then

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

        now

          let x;

          assume x in the carrier of V;

          then

          reconsider v = x as VECTOR of V;

          (g . v) in REAL ;

          hence x in D implies (l . x) in REAL ;

          assume not x in D;

          thus 0 in REAL by XREAL_0:def 1;

        end;

        then

         A6: for x be object st x in the carrier of V holds ( D[x] implies F(x) in REAL ) & ( not D[x] implies G(x) in REAL );

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

         A7: 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) = G(x)) from FUNCT_2:sch 5( A6);

        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 A7;

        then

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

        

         A8: D c= B

        proof

          let x be object;

          assume x in D;

          then

           A9: 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 A9, XBOOLE_0:def 3;

        end;

        ( Carrier g) c= D

        proof

          let x be object;

          assume x in ( Carrier g);

          then

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

          assume not x in D;

          hence thesis by A7, A10;

        end;

        then ( Carrier g) c= B by A8;

        then

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

        l = (f + g)

        proof

          let v;

          now

            per cases ;

              suppose

               A11: v in C;

               A12:

              now

                assume v in D;

                then not v in A by XBOOLE_0:def 5;

                hence contradiction by A11, XBOOLE_0:def 4;

              end;

              

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

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

              .= ((l . v) + 0 ) by A7, A12

              .= (l . v);

            end;

              suppose

               A13: not v in C;

              now

                per cases ;

                  suppose

                   A14: v in ( Carrier l);

                   A15:

                  now

                    assume not v in D;

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

                    hence contradiction by A13, A14, XBOOLE_0:def 4;

                  end;

                  

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

                  .= ( 0 + (g . v)) by A3, A13

                  .= (l . v) by A7, A15;

                end;

                  suppose

                   A16: not v in ( Carrier l);

                  then

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

                  

                   A18: not v in C by A16, XBOOLE_0:def 4;

                  

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

                  .= ( 0 + (g . v)) by A3, A18

                  .= ( 0 + 0 ) by A7, A17

                  .= (l . v) by A16;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        then

         A19: v = (( Sum f) + ( Sum g)) by A1, Th1;

        ( Sum f) in ( Lin A) & ( Sum g) in ( Lin B) by Th14;

        hence v in (( Lin A) + ( Lin B)) by A19, RLSUB_2: 1;

      end;

      then

       A20: ( Lin (A \/ B)) is Subspace of (( Lin A) + ( Lin B)) by RLSUB_1: 29;

      ( Lin A) is Subspace of ( Lin (A \/ B)) & ( Lin B) is Subspace of ( Lin (A \/ B)) by Th20, XBOOLE_1: 7;

      then (( Lin A) + ( Lin B)) is Subspace of ( Lin (A \/ B)) by Lm6;

      hence thesis by A20, RLSUB_1: 26;

    end;

    theorem :: RLVECT_3:23

    ( Lin (A /\ B)) is Subspace of (( Lin A) /\ ( Lin B))

    proof

      ( Lin (A /\ B)) is Subspace of ( Lin A) & ( Lin (A /\ B)) is Subspace of ( Lin B) by Th20, XBOOLE_1: 17;

      hence thesis by Lm4;

    end;

    

     Lm7: not {} in M implies ( dom CF) = M

    proof

      set x = the Element of M;

      

       A1: x in M;

      assume

       A2: not {} in M;

      then

       A3: CF is Function of M, ( union M) by ORDERS_1: 90;

      ( union M) <> {} by A1, ORDERS_1: 6, A2;

      hence thesis by FUNCT_2:def 1, A3;

    end;

    theorem :: RLVECT_3:24

    

     Th24: A is linearly-independent implies ex B st A c= B & B is linearly-independent & ( Lin B) = the RLSStruct of V

    proof

      defpred P[ set] means (ex B be Subset of V st B = $1 & A c= B & B is linearly-independent);

      consider Q be set such that

       A1: for Z holds Z in Q iff Z in ( bool the carrier of V) & P[Z] from XFAMILY:sch 1;

       A2:

      now

        let Z;

        assume that

         A3: Z <> {} and

         A4: Z c= Q and

         A5: Z is c=-linear;

        set W = ( union Z);

        W c= the carrier of V

        proof

          let x be object;

          assume x in W;

          then

          consider X such that

           A6: x in X and

           A7: X in Z by TARSKI:def 4;

          X in ( bool the carrier of V) by A1, A4, A7;

          hence thesis by A6;

        end;

        then

        reconsider W as Subset of V;

        

         A8: W is linearly-independent

        proof

          deffunc Q( object) = { C where C be Subset of V : $1 in C & C in Z };

          let l be Linear_Combination of W;

          assume that

           A9: ( Sum l) = ( 0. V) and

           A10: ( Carrier l) <> {} ;

          consider f be Function such that

           A11: ( dom f) = ( Carrier l) and

           A12: for x be object st x in ( Carrier l) holds (f . x) = Q(x) from FUNCT_1:sch 3;

          reconsider M = ( rng f) as non empty set by A10, A11, RELAT_1: 42;

          set F = the Choice_Function of M;

          set S = ( rng F);

           A13:

          now

            assume {} in M;

            then

            consider x be object such that

             A14: x in ( dom f) and

             A15: (f . x) = {} by FUNCT_1:def 3;

            ( Carrier l) c= W by RLVECT_2:def 6;

            then

            consider X such that

             A16: x in X and

             A17: X in Z by A11, A14, TARSKI:def 4;

            reconsider X as Subset of V by A1, A4, A17;

            X in { C where C be Subset of V : x in C & C in Z } by A16, A17;

            hence contradiction by A11, A12, A14, A15;

          end;

          then

           A18: ( dom F) = M by Lm7;

          then ( dom F) is finite by A11, FINSET_1: 8;

          then

           A19: S is finite by FINSET_1: 8;

           A20:

          now

            let X;

            assume X in S;

            then

            consider x be object such that

             A21: x in ( dom F) and

             A22: (F . x) = X by FUNCT_1:def 3;

            consider y be object such that

             A23: y in ( dom f) & (f . y) = x by A18, A21, FUNCT_1:def 3;

            

             A24: x = Q(y) by A11, A12, A23;

            reconsider x as set by TARSKI: 1;

            X in x by A13, A18, A21, A22, ORDERS_1: 89;

            then ex C be Subset of V st C = X & y in C & C in Z by A24;

            hence X in Z;

          end;

           A25:

          now

            let X, Y;

            assume X in S & Y in S;

            then X in Z & Y in Z by A20;

            then (X,Y) are_c=-comparable by A5, ORDINAL1:def 8;

            hence X c= Y or Y c= X;

          end;

          S <> {} by A18, RELAT_1: 42;

          then ( union S) in S by A25, A19, CARD_2: 62;

          then ( union S) in Z by A20;

          then

          consider B be Subset of V such that

           A26: B = ( union S) and A c= B and

           A27: B is linearly-independent by A1, A4;

          ( Carrier l) c= ( union S)

          proof

            let x be object;

            set X = (f . x);

            assume

             A28: x in ( Carrier l);

            then

             A29: (f . x) = { C where C be Subset of V : x in C & C in Z } by A12;

            

             A30: (f . x) in M by A11, A28, FUNCT_1:def 3;

            then (F . X) in X by A13, ORDERS_1: 89;

            then

             A31: ex C be Subset of V st (F . X) = C & x in C & C in Z by A29;

            (F . X) in S by A18, A30, FUNCT_1:def 3;

            hence thesis by A31, TARSKI:def 4;

          end;

          then l is Linear_Combination of B by A26, RLVECT_2:def 6;

          hence thesis by A9, A10, A27;

        end;

        set x = the Element of Z;

        x in Q by A3, A4;

        then

         A32: ex B be Subset of V st B = x & A c= B & B is linearly-independent by A1;

        x c= W by A3, ZFMISC_1: 74;

        then A c= W by A32;

        hence ( union Z) in Q by A1, A8;

      end;

      

       A33: ( (Omega). V) = the RLSStruct of V;

      assume A is linearly-independent;

      then Q <> {} by A1;

      then

      consider X such that

       A34: X in Q and

       A35: for Z st Z in Q & Z <> X holds not X c= Z by A2, ORDERS_1: 67;

      consider B be Subset of V such that

       A36: B = X and

       A37: A c= B and

       A38: B is linearly-independent by A1, A34;

      take B;

      thus A c= B & B is linearly-independent by A37, A38;

      assume ( Lin B) <> the RLSStruct of V;

      then

      consider v be VECTOR of V such that

       A39: not (v in ( Lin B) iff v in the RLSStruct of V) by A33, RLSUB_1: 31;

      

       A40: (B \/ {v}) is linearly-independent

      proof

        let l be Linear_Combination of (B \/ {v});

        assume

         A41: ( Sum l) = ( 0. V);

        now

          per cases ;

            suppose v in ( Carrier l);

            then

             A42: ( - (l . v)) <> 0 by RLVECT_2: 19;

            deffunc G( VECTOR of V) = ( In ( 0 , REAL ));

            deffunc L( VECTOR of V) = (l . $1);

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

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

             A44: for u be VECTOR of V st u <> v holds (f . u) = L(u) from FUNCT_2:sch 6;

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

            now

              let u be VECTOR of V;

              assume not u in (( Carrier l) \ {v});

              then not u in ( Carrier l) or u in {v} by XBOOLE_0:def 5;

              then (l . u) = 0 & u <> v or u = v by TARSKI:def 1;

              hence (f . u) = 0 by A43, A44;

            end;

            then

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

            ( Carrier f) c= B

            proof

              let x be object;

              

               A45: ( Carrier l) c= (B \/ {v}) by RLVECT_2:def 6;

              assume x in ( Carrier f);

              then

              consider u be VECTOR of V such that

               A46: u = x and

               A47: (f . u) <> 0 ;

              (f . u) = (l . u) by A43, A44, A47;

              then u in ( Carrier l) by A47;

              then u in B or u in {v} by A45, XBOOLE_0:def 3;

              hence thesis by A43, A46, A47, TARSKI:def 1;

            end;

            then

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

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

             A48: (g . v) = ( - (l . v)) and

             A49: for u be VECTOR of V st u <> v holds (g . u) = G(u) from FUNCT_2:sch 6;

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

            now

              let u be VECTOR of V;

              assume not u in {v};

              then u <> v by TARSKI:def 1;

              hence (g . u) = 0 by A49;

            end;

            then

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

            ( Carrier g) c= {v}

            proof

              let x be object;

              assume x in ( Carrier g);

              then ex u be VECTOR of V st x = u & (g . u) <> 0 ;

              then x = v by A49;

              hence thesis by TARSKI:def 1;

            end;

            then

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

            

             A50: ( Sum g) = (( - (l . v)) * v) by A48, RLVECT_2: 32;

            (f - g) = l

            proof

              let u be VECTOR of V;

              now

                per cases ;

                  suppose

                   A51: v = u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by RLVECT_2: 54

                  .= (l . u) by A43, A48, A51;

                end;

                  suppose

                   A52: v <> u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by RLVECT_2: 54

                  .= ((l . u) - (g . u)) by A44, A52

                  .= ((l . u) - 0 ) by A49, A52

                  .= (l . u);

                end;

              end;

              hence thesis;

            end;

            then ( 0. V) = (( Sum f) - ( Sum g)) by A41, Th4;

            

            then ( Sum f) = (( 0. V) + ( Sum g)) by RLSUB_2: 61

            .= (( - (l . v)) * v) by A50;

            then

             A53: (( - (l . v)) * v) in ( Lin B) by Th14;

            ((( - (l . v)) " ) * (( - (l . v)) * v)) = (((( - (l . v)) " ) * ( - (l . v))) * v) by RLVECT_1:def 7

            .= (1 * v) by A42, XCMPLX_0:def 7

            .= v by RLVECT_1:def 8;

            hence thesis by A39, A53, RLSUB_1: 21, RLVECT_1: 1;

          end;

            suppose

             A54: not v in ( Carrier l);

            ( Carrier l) c= B

            proof

              let x be object;

              assume

               A55: x in ( Carrier l);

              ( Carrier l) c= (B \/ {v}) by RLVECT_2:def 6;

              then x in B or x in {v} by A55, XBOOLE_0:def 3;

              hence thesis by A54, A55, TARSKI:def 1;

            end;

            then l is Linear_Combination of B by RLVECT_2:def 6;

            hence thesis by A38, A41;

          end;

        end;

        hence thesis;

      end;

      v in {v} by TARSKI:def 1;

      then

       A56: v in (B \/ {v}) by XBOOLE_0:def 3;

      

       A57: not v in B by A39, Th15, RLVECT_1: 1;

      B c= (B \/ {v}) by XBOOLE_1: 7;

      then A c= (B \/ {v}) by A37;

      then (B \/ {v}) in Q by A1, A40;

      hence contradiction by A35, A36, A56, A57, XBOOLE_1: 7;

    end;

    theorem :: RLVECT_3:25

    

     Th25: ( Lin A) = V implies ex B st B c= A & B is linearly-independent & ( Lin B) = V

    proof

      assume

       A1: ( Lin A) = V;

      defpred P[ set] means (ex B st B = $1 & B c= A & B is linearly-independent);

      consider Q be set such that

       A2: for Z holds Z in Q iff Z in ( bool the carrier of V) & P[Z] from XFAMILY:sch 1;

       A3:

      now

        let Z;

        assume that Z <> {} and

         A4: Z c= Q and

         A5: Z is c=-linear;

        set W = ( union Z);

        W c= the carrier of V

        proof

          let x be object;

          assume x in W;

          then

          consider X such that

           A6: x in X and

           A7: X in Z by TARSKI:def 4;

          X in ( bool the carrier of V) by A2, A4, A7;

          hence thesis by A6;

        end;

        then

        reconsider W as Subset of V;

        

         A8: W is linearly-independent

        proof

          deffunc F( object) = { C : $1 in C & C in Z };

          let l be Linear_Combination of W;

          assume that

           A9: ( Sum l) = ( 0. V) and

           A10: ( Carrier l) <> {} ;

          consider f be Function such that

           A11: ( dom f) = ( Carrier l) and

           A12: for x be object st x in ( Carrier l) holds (f . x) = F(x) from FUNCT_1:sch 3;

          reconsider M = ( rng f) as non empty set by A10, A11, RELAT_1: 42;

          set F = the Choice_Function of M;

          set S = ( rng F);

           A13:

          now

            assume {} in M;

            then

            consider x be object such that

             A14: x in ( dom f) and

             A15: (f . x) = {} by FUNCT_1:def 3;

            ( Carrier l) c= W by RLVECT_2:def 6;

            then

            consider X such that

             A16: x in X and

             A17: X in Z by A11, A14, TARSKI:def 4;

            reconsider X as Subset of V by A2, A4, A17;

            X in { C : x in C & C in Z } by A16, A17;

            hence contradiction by A11, A12, A14, A15;

          end;

          then

           A18: ( dom F) = M by Lm7;

          then ( dom F) is finite by A11, FINSET_1: 8;

          then

           A19: S is finite by FINSET_1: 8;

           A20:

          now

            let X;

            assume X in S;

            then

            consider x be object such that

             A21: x in ( dom F) and

             A22: (F . x) = X by FUNCT_1:def 3;

            consider y be object such that

             A23: y in ( dom f) & (f . y) = x by A18, A21, FUNCT_1:def 3;

            

             A24: x = { C : y in C & C in Z } by A11, A12, A23;

            reconsider x as set by TARSKI: 1;

            X in x by A13, A18, A21, A22, ORDERS_1: 89;

            then ex C st C = X & y in C & C in Z by A24;

            hence X in Z;

          end;

           A25:

          now

            let X, Y;

            assume X in S & Y in S;

            then X in Z & Y in Z by A20;

            then (X,Y) are_c=-comparable by A5, ORDINAL1:def 8;

            hence X c= Y or Y c= X;

          end;

          S <> {} by A18, RELAT_1: 42;

          then ( union S) in S by A25, A19, CARD_2: 62;

          then ( union S) in Z by A20;

          then

          consider B such that

           A26: B = ( union S) and B c= A and

           A27: B is linearly-independent by A2, A4;

          ( Carrier l) c= ( union S)

          proof

            let x be object;

            set X = (f . x);

            assume

             A28: x in ( Carrier l);

            then

             A29: (f . x) = { C : x in C & C in Z } by A12;

            

             A30: (f . x) in M by A11, A28, FUNCT_1:def 3;

            then (F . X) in X by A13, ORDERS_1: 89;

            then

             A31: ex C st (F . X) = C & x in C & C in Z by A29;

            (F . X) in S by A18, A30, FUNCT_1:def 3;

            hence thesis by A31, TARSKI:def 4;

          end;

          then l is Linear_Combination of B by A26, RLVECT_2:def 6;

          hence thesis by A9, A10, A27;

        end;

        W c= A

        proof

          let x be object;

          assume x in W;

          then

          consider X such that

           A32: x in X and

           A33: X in Z by TARSKI:def 4;

          ex B st B = X & B c= A & B is linearly-independent by A2, A4, A33;

          hence thesis by A32;

        end;

        hence ( union Z) in Q by A2, A8;

      end;

      ( {} the carrier of V) c= A & ( {} the carrier of V) is linearly-independent by Th7;

      then Q <> {} by A2;

      then

      consider X such that

       A34: X in Q and

       A35: for Z st Z in Q & Z <> X holds not X c= Z by A3, ORDERS_1: 67;

      consider B such that

       A36: B = X and

       A37: B c= A and

       A38: B is linearly-independent by A2, A34;

      take B;

      thus B c= A & B is linearly-independent by A37, A38;

      assume

       A39: ( Lin B) <> V;

      now

        assume

         A40: for v st v in A holds v in ( Lin B);

        now

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

          let v;

          assume v in ( Lin A);

          then

          consider l such that

           A41: v = ( Sum l) by Th14;

          ( Carrier l) c= the carrier of ( Lin B)

          proof

            let x be object;

            assume

             A42: x in ( Carrier l);

            then

            reconsider a = x as VECTOR of V;

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

            then a in ( Lin B) by A40, A42;

            hence thesis by STRUCT_0:def 5;

          end;

          then

          reconsider l as Linear_Combination of F by RLVECT_2:def 6;

          ( Sum l) = v by A41;

          then v in ( Lin F) by Th14;

          hence v in ( Lin B) by Th18;

        end;

        then ( Lin A) is Subspace of ( Lin B) by RLSUB_1: 29;

        hence contradiction by A1, A39, RLSUB_1: 26;

      end;

      then

      consider v such that

       A43: v in A and

       A44: not v in ( Lin B);

      

       A45: (B \/ {v}) is linearly-independent

      proof

        let l be Linear_Combination of (B \/ {v});

        assume

         A46: ( Sum l) = ( 0. V);

        now

          per cases ;

            suppose v in ( Carrier l);

            then

             A47: ( - (l . v)) <> 0 by RLVECT_2: 19;

            deffunc G( VECTOR of V) = ( In ( 0 , REAL ));

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

            consider f such that

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

             A49: for u 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 (( Carrier l) \ {v});

              then not u in ( Carrier l) or u in {v} by XBOOLE_0:def 5;

              then (l . u) = 0 & u <> v or u = v by TARSKI:def 1;

              hence (f . u) = 0 by A48, A49;

            end;

            then

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

            ( Carrier f) c= B

            proof

              let x be object;

              

               A50: ( Carrier l) c= (B \/ {v}) by RLVECT_2:def 6;

              assume x in ( Carrier f);

              then

              consider u such that

               A51: u = x and

               A52: (f . u) <> 0 ;

              (f . u) = (l . u) by A48, A49, A52;

              then u in ( Carrier l) by A52;

              then u in B or u in {v} by A50, XBOOLE_0:def 3;

              hence thesis by A48, A51, A52, TARSKI:def 1;

            end;

            then

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

            consider g such that

             A53: (g . v) = ( - (l . v)) and

             A54: for u st u <> v holds (g . u) = G(u) from FUNCT_2:sch 6;

            reconsider g 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 (g . u) = 0 by A54;

            end;

            then

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

            ( Carrier g) c= {v}

            proof

              let x be object;

              assume x in ( Carrier g);

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

              then x = v by A54;

              hence thesis by TARSKI:def 1;

            end;

            then

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

            

             A55: ( Sum g) = (( - (l . v)) * v) by A53, RLVECT_2: 32;

            (f - g) = l

            proof

              let u;

              now

                per cases ;

                  suppose

                   A56: v = u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by RLVECT_2: 54

                  .= (l . u) by A48, A53, A56;

                end;

                  suppose

                   A57: v <> u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by RLVECT_2: 54

                  .= ((l . u) - (g . u)) by A49, A57

                  .= ((l . u) - 0 ) by A54, A57

                  .= (l . u);

                end;

              end;

              hence thesis;

            end;

            then ( 0. V) = (( Sum f) - ( Sum g)) by A46, Th4;

            

            then ( Sum f) = (( 0. V) + ( Sum g)) by RLSUB_2: 61

            .= (( - (l . v)) * v) by A55;

            then

             A58: (( - (l . v)) * v) in ( Lin B) by Th14;

            ((( - (l . v)) " ) * (( - (l . v)) * v)) = (((( - (l . v)) " ) * ( - (l . v))) * v) by RLVECT_1:def 7

            .= (1 * v) by A47, XCMPLX_0:def 7

            .= v by RLVECT_1:def 8;

            hence thesis by A44, A58, RLSUB_1: 21;

          end;

            suppose

             A59: not v in ( Carrier l);

            ( Carrier l) c= B

            proof

              let x be object;

              assume

               A60: x in ( Carrier l);

              ( Carrier l) c= (B \/ {v}) by RLVECT_2:def 6;

              then x in B or x in {v} by A60, XBOOLE_0:def 3;

              hence thesis by A59, A60, TARSKI:def 1;

            end;

            then l is Linear_Combination of B by RLVECT_2:def 6;

            hence thesis by A38, A46;

          end;

        end;

        hence thesis;

      end;

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

      then (B \/ {v}) c= A by A37, XBOOLE_1: 8;

      then

       A61: (B \/ {v}) in Q by A2, A45;

      v in {v} by TARSKI:def 1;

      then

       A62: v in (B \/ {v}) by XBOOLE_0:def 3;

       not v in B by A44, Th15;

      hence contradiction by A35, A36, A62, A61, XBOOLE_1: 7;

    end;

    definition

      let V be RealLinearSpace;

      :: RLVECT_3:def3

      mode Basis of V -> Subset of V means

      : Def3: it is linearly-independent & ( Lin it ) = the RLSStruct of V;

      existence

      proof

        ( {} the carrier of V) is linearly-independent by Th7;

        then ex B be Subset of V st ( {} the carrier of V) c= B & B is linearly-independent & ( Lin B) = the RLSStruct of V by Th24;

        hence thesis;

      end;

    end

    reserve I for Basis of V;

    theorem :: RLVECT_3:26

    for V be strict RealLinearSpace, A be Subset of V holds A is linearly-independent implies ex I be Basis of V st A c= I

    proof

      let V be strict RealLinearSpace, A be Subset of V;

      assume A is linearly-independent;

      then

      consider B be Subset of V such that

       A1: A c= B and

       A2: B is linearly-independent & ( Lin B) = V by Th24;

      reconsider B as Basis of V by A2, Def3;

      take B;

      thus thesis by A1;

    end;

    theorem :: RLVECT_3:27

    ( Lin A) = V implies ex I st I c= A

    proof

      assume ( Lin A) = V;

      then

      consider B such that

       A1: B c= A and

       A2: B is linearly-independent & ( Lin B) = V by Th25;

      reconsider B as Basis of V by A2, Def3;

      take B;

      thus thesis by A1;

    end;

    theorem :: RLVECT_3:28

     not {} in M implies ( dom CF) = M by Lm7;

    theorem :: RLVECT_3:29

    x in ( (0). V) iff x = ( 0. V) by Lm2;

    theorem :: RLVECT_3:30

    W1 is Subspace of W3 implies (W1 /\ W2) is Subspace of W3 by Lm3;

    theorem :: RLVECT_3:31

    W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of (W2 /\ W3) by Lm4;

    theorem :: RLVECT_3:32

    W1 is Subspace of W3 & W2 is Subspace of W3 implies (W1 + W2) is Subspace of W3 by Lm6;

    theorem :: RLVECT_3:33

    W1 is Subspace of W2 implies W1 is Subspace of (W2 + W3) by Lm5;

    theorem :: RLVECT_3:34

    (f (#) (F ^ G)) = ((f (#) F) ^ (f (#) G)) by Lm1;