rusub_4.miz



    begin

    theorem :: RUSUB_4:1

    

     Th1: for V be RealUnitarySpace, A,B be finite Subset of V, v be VECTOR of V st v in ( Lin (A \/ B)) & not v in ( Lin B) holds ex w be VECTOR of V st w in A & w in ( Lin (((A \/ B) \ {w}) \/ {v}))

    proof

      let V be RealUnitarySpace;

      let A,B be finite Subset of V;

      let v be VECTOR of V such that

       A1: v in ( Lin (A \/ B)) and

       A2: not v in ( Lin B);

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

       A3: v = ( Sum L) by A1, RUSUB_3: 1;

      v in {v} by TARSKI:def 1;

      then v in ( Lin {v}) by RUSUB_3: 2;

      then

      consider Lv be Linear_Combination of {v} such that

       A4: v = ( Sum Lv) by RUSUB_3: 1;

      

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

      now

        assume

         A6: for w be VECTOR of V st w in A holds (L . w) = 0 ;

        now

          let x be object;

          assume that

           A7: x in ( Carrier L) and

           A8: x in A;

          ex u be VECTOR of V st x = u & (L . u) <> 0 by A7, RLVECT_5: 3;

          hence contradiction by A6, A8;

        end;

        then ( Carrier L) misses A by XBOOLE_0: 3;

        then ( Carrier L) c= B by A5, XBOOLE_1: 73;

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

        hence contradiction by A2, A3, RUSUB_3: 1;

      end;

      then

      consider w be VECTOR of V such that

       A9: w in A and

       A10: (L . w) <> 0 ;

      consider F be FinSequence of the carrier of V such that

       A11: F is one-to-one and

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

       A13: ( Sum L) = ( Sum (L (#) F)) by RLVECT_2:def 8;

      

       A14: w in ( rng F) by A10, A12, RLVECT_5: 3;

      then

      reconsider Fw1 = (F -| w) as FinSequence of the carrier of V by FINSEQ_4: 41;

      reconsider Fw2 = (F |-- w) as FinSequence of the carrier of V by A14, FINSEQ_4: 50;

      

       A15: ( rng Fw1) misses ( rng Fw2) by A11, A14, FINSEQ_4: 57;

      set Fw = (Fw1 ^ Fw2);

      consider K be Linear_Combination of V such that

       A16: ( Carrier K) = (( rng Fw) /\ ( Carrier L)) and

       A17: (L (#) Fw) = (K (#) Fw) by RLVECT_5: 7;

      F just_once_values w by A11, A14, FINSEQ_4: 8;

      then Fw = (F - {w}) by FINSEQ_4: 54;

      then

       A18: ( rng Fw) = (( Carrier L) \ {w}) by A12, FINSEQ_3: 65;

      then

       A19: ( Carrier K) = ( rng Fw) by A16, XBOOLE_1: 28, XBOOLE_1: 36;

      then

       A20: ( Carrier K) c= ((A \/ B) \ {w}) by A5, A18, XBOOLE_1: 33;

      take w;

      set a = (L . w);

      

       A21: (a " ) <> 0 by A10, XCMPLX_1: 202;

      F = (((F -| w) ^ <*w*>) ^ (F |-- w)) by A14, FINSEQ_4: 51;

      then F = (Fw1 ^ ( <*w*> ^ Fw2)) by FINSEQ_1: 32;

      

      then (L (#) F) = ((L (#) Fw1) ^ (L (#) ( <*w*> ^ Fw2))) by RLVECT_3: 34

      .= ((L (#) Fw1) ^ ((L (#) <*w*>) ^ (L (#) Fw2))) by RLVECT_3: 34

      .= (((L (#) Fw1) ^ (L (#) <*w*>)) ^ (L (#) Fw2)) by FINSEQ_1: 32

      .= (((L (#) Fw1) ^ <*(a * w)*>) ^ (L (#) Fw2)) by RLVECT_2: 26;

      

      then

       A22: ( Sum (L (#) F)) = ( Sum ((L (#) Fw1) ^ ( <*(a * w)*> ^ (L (#) Fw2)))) by FINSEQ_1: 32

      .= (( Sum (L (#) Fw1)) + ( Sum ( <*(a * w)*> ^ (L (#) Fw2)))) by RLVECT_1: 41

      .= (( Sum (L (#) Fw1)) + (( Sum <*(a * w)*>) + ( Sum (L (#) Fw2)))) by RLVECT_1: 41

      .= (( Sum (L (#) Fw1)) + (( Sum (L (#) Fw2)) + (a * w))) by RLVECT_1: 44

      .= ((( Sum (L (#) Fw1)) + ( Sum (L (#) Fw2))) + (a * w)) by RLVECT_1:def 3

      .= (( Sum ((L (#) Fw1) ^ (L (#) Fw2))) + (a * w)) by RLVECT_1: 41

      .= (( Sum (L (#) (Fw1 ^ Fw2))) + (a * w)) by RLVECT_3: 34;

      reconsider K as Linear_Combination of ((A \/ B) \ {w}) by A20, RLVECT_2:def 6;

      ( Carrier (( - K) + Lv)) c= (( Carrier ( - K)) \/ ( Carrier Lv)) by RLVECT_2: 37;

      then

       A23: ( Carrier (( - K) + Lv)) c= (( Carrier K) \/ ( Carrier Lv)) by RLVECT_2: 51;

      set LC = ((a " ) * (( - K) + Lv));

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

      then (( Carrier K) \/ ( Carrier Lv)) c= (((A \/ B) \ {w}) \/ {v}) by A20, XBOOLE_1: 13;

      then ( Carrier (( - K) + Lv)) c= (((A \/ B) \ {w}) \/ {v}) by A23;

      then ( Carrier LC) c= (((A \/ B) \ {w}) \/ {v}) by A21, RLVECT_2: 42;

      then

       A24: LC is Linear_Combination of (((A \/ B) \ {w}) \/ {v}) by RLVECT_2:def 6;

      Fw1 is one-to-one & Fw2 is one-to-one by A11, A14, FINSEQ_4: 52, FINSEQ_4: 53;

      then Fw is one-to-one by A15, FINSEQ_3: 91;

      then ( Sum (K (#) Fw)) = ( Sum K) by A19, RLVECT_2:def 8;

      

      then ((a " ) * v) = (((a " ) * ( Sum K)) + ((a " ) * (a * w))) by A3, A13, A22, A17, RLVECT_1:def 5

      .= (((a " ) * ( Sum K)) + (((a " ) * a) * w)) by RLVECT_1:def 7

      .= (((a " ) * ( Sum K)) + (1 * w)) by A10, XCMPLX_0:def 7

      .= (((a " ) * ( Sum K)) + w) by RLVECT_1:def 8;

      

      then w = (((a " ) * v) - ((a " ) * ( Sum K))) by RLSUB_2: 61

      .= ((a " ) * (v - ( Sum K))) by RLVECT_1: 34

      .= ((a " ) * (( - ( Sum K)) + v)) by RLVECT_1:def 11;

      

      then w = ((a " ) * (( Sum ( - K)) + ( Sum Lv))) by A4, RLVECT_3: 3

      .= ((a " ) * ( Sum (( - K) + Lv))) by RLVECT_3: 1

      .= ( Sum ((a " ) * (( - K) + Lv))) by RLVECT_3: 2;

      hence thesis by A9, A24, RUSUB_3: 1;

    end;

    

     Lm1: for X be set, x be set st x in X holds ((X \ {x}) \/ {x}) = X

    proof

      let X be set;

      let x be set;

      assume x in X;

      then

       A1: {x} is Subset of X by SUBSET_1: 41;

      ( {x} \/ (X \ {x})) = ( {x} \/ X) by XBOOLE_1: 39

      .= X by A1, XBOOLE_1: 12;

      hence thesis;

    end;

    theorem :: RUSUB_4:2

    

     Th2: for V be RealUnitarySpace, A,B be finite Subset of V st the UNITSTR of V = ( Lin A) & B is linearly-independent holds ( card B) <= ( card A) & ex C be finite Subset of V st C c= A & ( card C) = (( card A) - ( card B)) & the UNITSTR of V = ( Lin (B \/ C))

    proof

      let V be RealUnitarySpace;

      defpred P[ Nat] means for n be Element of NAT holds for A,B be finite Subset of V st ( card A) = n & ( card B) = $1 & the UNITSTR of V = ( Lin A) & B is linearly-independent holds $1 <= n & ex C be finite Subset of V st C c= A & ( card C) = (n - $1) & the UNITSTR of V = ( Lin (B \/ C));

      

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

      proof

        let m be Nat such that

         A2: P[m];

        let n be Element of NAT ;

        let A,B be finite Subset of V such that

         A3: ( card A) = n and

         A4: ( card B) = (m + 1) and

         A5: the UNITSTR of V = ( Lin A) and

         A6: B is linearly-independent;

        consider v be object such that

         A7: v in B by A4, CARD_1: 27, XBOOLE_0:def 1;

        reconsider v as VECTOR of V by A7;

        set Bv = (B \ {v});

        

         A8: Bv is linearly-independent by A6, RLVECT_3: 5, XBOOLE_1: 36;

         {v} is Subset of B by A7, SUBSET_1: 41;

        

        then

         A9: ( card (B \ {v})) = (( card B) - ( card {v})) by CARD_2: 44

        .= ((m + 1) - 1) by A4, CARD_1: 30

        .= m;

        then

        consider C be finite Subset of V such that

         A10: C c= A and

         A11: ( card C) = (n - m) and

         A12: the UNITSTR of V = ( Lin (Bv \/ C)) by A2, A3, A5, A8;

        

         A13: not v in ( Lin Bv) by A6, A7, RUSUB_3: 25;

         A14:

        now

          assume m = n;

          then

          consider C be finite Subset of V such that C c= A and

           A15: ( card C) = (m - m) and

           A16: the UNITSTR of V = ( Lin (Bv \/ C)) by A2, A3, A5, A9, A8;

          C = {} by A15;

          then Bv is Basis of V by A8, A16, RUSUB_3:def 2;

          hence contradiction by A13, RUSUB_3: 21;

        end;

        v in ( Lin (Bv \/ C)) by A12;

        then

        consider w be VECTOR of V such that

         A17: w in C and

         A18: w in ( Lin (((C \/ Bv) \ {w}) \/ {v})) by A13, Th1;

        set Cw = (C \ {w});

        ((Bv \ {w}) \/ {v}) c= (Bv \/ {v}) by XBOOLE_1: 9, XBOOLE_1: 36;

        then (Cw \/ ((Bv \ {w}) \/ {v})) c= (Cw \/ (Bv \/ {v})) by XBOOLE_1: 9;

        then

         A19: (Cw \/ ((Bv \ {w}) \/ {v})) c= (B \/ Cw) by A7, Lm1;

         {w} is Subset of C by A17, SUBSET_1: 41;

        

        then

         A20: ( card Cw) = (( card C) - ( card {w})) by CARD_2: 44

        .= ((n - m) - 1) by A11, CARD_1: 30

        .= (n - (m + 1));

        Cw c= C by XBOOLE_1: 36;

        then

         A21: Cw c= A by A10;

        (((C \/ Bv) \ {w}) \/ {v}) = ((Cw \/ (Bv \ {w})) \/ {v}) by XBOOLE_1: 42

        .= (Cw \/ ((Bv \ {w}) \/ {v})) by XBOOLE_1: 4;

        then ( Lin (((C \/ Bv) \ {w}) \/ {v})) is Subspace of ( Lin (B \/ Cw)) by A19, RUSUB_3: 7;

        then

         A22: w in ( Lin (B \/ Cw)) by A18, RUSUB_1: 1;

        

         A23: Bv c= B & C = (Cw \/ {w}) by A17, Lm1, XBOOLE_1: 36;

        now

          let x be object;

          assume x in (Bv \/ C);

          then x in Bv or x in C by XBOOLE_0:def 3;

          then x in B or x in Cw or x in {w} by A23, XBOOLE_0:def 3;

          then x in (B \/ Cw) or x in {w} by XBOOLE_0:def 3;

          then x in ( Lin (B \/ Cw)) or x = w by RUSUB_3: 2, TARSKI:def 1;

          hence x in the carrier of ( Lin (B \/ Cw)) by A22;

        end;

        then (Bv \/ C) c= the carrier of ( Lin (B \/ Cw));

        then ( Lin (Bv \/ C)) is Subspace of ( Lin (B \/ Cw)) by RUSUB_3: 27;

        then

         A24: the carrier of ( Lin (Bv \/ C)) c= the carrier of ( Lin (B \/ Cw)) by RUSUB_1:def 1;

        the carrier of ( Lin (B \/ Cw)) c= the carrier of V by RUSUB_1:def 1;

        then the carrier of ( Lin (B \/ Cw)) = the carrier of V by A12, A24;

        then

         A25: the UNITSTR of V = ( Lin (B \/ Cw)) by A12, RUSUB_1: 24;

        m <= n by A2, A3, A5, A9, A8;

        then m < n by A14, XXREAL_0: 1;

        hence thesis by A21, A20, A25, NAT_1: 13;

      end;

      

       A26: P[ 0 ]

      proof

        let n be Element of NAT ;

        let A,B be finite Subset of V such that

         A27: ( card A) = n and

         A28: ( card B) = 0 and

         A29: the UNITSTR of V = ( Lin A) and B is linearly-independent;

        B = {} by A28;

        then A = (B \/ A);

        hence thesis by A27, A29;

      end;

      

       A30: for m be Nat holds P[m] from NAT_1:sch 2( A26, A1);

      let A,B be finite Subset of V;

      assume the UNITSTR of V = ( Lin A) & B is linearly-independent;

      hence thesis by A30;

    end;

    definition

      let V be RealUnitarySpace;

      :: RUSUB_4:def1

      attr V is finite-dimensional means

      : Def1: ex A be finite Subset of V st A is Basis of V;

    end

    registration

      cluster strict finite-dimensional for RealUnitarySpace;

      existence

      proof

        set V = the RealUnitarySpace;

        take ( (0). V);

        thus ( (0). V) is strict;

        take A = ( {} the carrier of ( (0). V));

        ( Lin A) = ( (0). ( (0). V)) by RUSUB_3: 3;

        then A is linearly-independent & ( Lin A) = the UNITSTR of ( (0). V) by RLVECT_3: 7, RUSUB_1: 30;

        hence thesis by RUSUB_3:def 2;

      end;

    end

    theorem :: RUSUB_4:3

    

     Th3: for V be RealUnitarySpace st V is finite-dimensional holds for I be Basis of V holds I is finite

    proof

      let V be RealUnitarySpace;

      assume V is finite-dimensional;

      then

      consider A be finite Subset of V such that

       A1: A is Basis of V;

      let B be Basis of V;

      consider p be FinSequence such that

       A2: ( rng p) = A by FINSEQ_1: 52;

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

      set Car = { ( Carrier L) where L be Linear_Combination of B : ex i be Element of NAT st i in ( dom p) & ( Sum L) = (p . i) };

      set C = ( union Car);

      

       A3: C c= B

      proof

        let x be object;

        assume x in C;

        then

        consider R be set such that

         A4: x in R and

         A5: R in Car by TARSKI:def 4;

        ex L be Linear_Combination of B st R = ( Carrier L) & ex i be Element of NAT st i in ( dom p) & ( Sum L) = (p . i) by A5;

        then R c= B by RLVECT_2:def 6;

        hence thesis by A4;

      end;

      then

      reconsider C as Subset of V by XBOOLE_1: 1;

      for v be VECTOR of V holds v in ( (Omega). V) iff v in ( Lin C)

      proof

        let v be VECTOR of V;

        hereby

          assume v in ( (Omega). V);

          v in the UNITSTR of V;

          then v in ( Lin A) by A1, RUSUB_3:def 2;

          then

          consider LA be Linear_Combination of A such that

           A6: v = ( Sum LA) by RUSUB_3: 1;

          ( Carrier LA) c= the carrier of ( Lin C)

          proof

            let w be object;

            assume

             A7: w in ( Carrier LA);

            then

            reconsider w9 = w as VECTOR of V;

            w9 in ( Lin B) by RUSUB_3: 21;

            then

            consider LB be Linear_Combination of B such that

             A8: w = ( Sum LB) by RUSUB_3: 1;

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

            then ex i be object st i in ( dom p) & w = (p . i) by A2, A7, FUNCT_1:def 3;

            then

             A9: ( Carrier LB) in Car by A8;

            ( Carrier LB) c= C by A9, TARSKI:def 4;

            then LB is Linear_Combination of C by RLVECT_2:def 6;

            then w in ( Lin C) by A8, RUSUB_3: 1;

            hence thesis;

          end;

          then ex LC be Linear_Combination of C st ( Sum LA) = ( Sum LC) by RUSUB_3: 17;

          hence v in ( Lin C) by A6, RUSUB_3: 1;

        end;

        assume v in ( Lin C);

        v in the carrier of the UNITSTR of V;

        then v in the carrier of ( (Omega). V) by RUSUB_1:def 3;

        hence thesis;

      end;

      then ( (Omega). V) = ( Lin C) by RUSUB_1: 25;

      then

       A10: the UNITSTR of V = ( Lin C) by RUSUB_1:def 3;

      

       A11: B is linearly-independent by RUSUB_3:def 2;

      then C is linearly-independent by A3, RLVECT_3: 5;

      then

       A12: C is Basis of V by A10, RUSUB_3:def 2;

      B c= C

      proof

        set D = (B \ C);

        assume not B c= C;

        then ex v be object st v in B & not v in C;

        then

        reconsider D as non empty Subset of V by XBOOLE_0:def 5;

        reconsider B as Subset of V;

        (C \/ (B \ C)) = (C \/ B) by XBOOLE_1: 39

        .= B by A3, XBOOLE_1: 12;

        then B = (C \/ D);

        hence contradiction by A11, A12, RUSUB_3: 26, XBOOLE_1: 79;

      end;

      then

       A13: B = C by A3;

      defpred P[ set, object] means ex L be Linear_Combination of B st $2 = ( Carrier L) & ( Sum L) = (p . $1);

      

       A14: for i be Nat st i in ( Seg ( len p)) holds ex x be object st P[i, x]

      proof

        let i be Nat;

        assume i in ( Seg ( len p));

        then i in ( dom p) by FINSEQ_1:def 3;

        then (p . i) in the carrier of V by FINSEQ_2: 11;

        then (p . i) in ( Lin B) by RUSUB_3: 21;

        then

        consider L be Linear_Combination of B such that

         A15: (p . i) = ( Sum L) by RUSUB_3: 1;

         P[i, ( Carrier L)] by A15;

        hence thesis;

      end;

      ex q be FinSequence st ( dom q) = ( Seg ( len p)) & for i be Nat st i in ( Seg ( len p)) holds P[i, (q . i)] from FINSEQ_1:sch 1( A14);

      then

      consider q be FinSequence such that

       A16: ( dom q) = ( Seg ( len p)) and

       A17: for i be Nat st i in ( Seg ( len p)) holds P[i, (q . i)];

      

       A18: ( dom p) = ( dom q) by A16, FINSEQ_1:def 3;

      

       A19: for i be Nat, y1,y2 be set st i in ( Seg ( len p)) & P[i, y1] & P[i, y2] holds y1 = y2

      proof

        let i be Nat;

        let y1,y2 be set;

        assume that i in ( Seg ( len p)) and

         A20: P[i, y1] and

         A21: P[i, y2];

        consider L1 be Linear_Combination of B such that

         A22: y1 = ( Carrier L1) & ( Sum L1) = (p . i) by A20;

        consider L2 be Linear_Combination of B such that

         A23: y2 = ( Carrier L2) & ( Sum L2) = (p . i) by A21;

        ( Carrier L1) c= B & ( Carrier L2) c= B by RLVECT_2:def 6;

        hence thesis by A11, A22, A23, RLVECT_5: 1;

      end;

      now

        let x be object;

        assume x in Car;

        then

        consider L be Linear_Combination of B such that

         A24: x = ( Carrier L) and

         A25: ex i be Element of NAT st i in ( dom p) & ( Sum L) = (p . i);

        consider i be Element of NAT such that

         A26: i in ( dom p) and

         A27: ( Sum L) = (p . i) by A25;

         P[i, (q . i)] by A16, A17, A18, A26;

        then x = (q . i) by A19, A16, A18, A24, A26, A27;

        hence x in ( rng q) by A18, A26, FUNCT_1:def 3;

      end;

      then

       A28: Car c= ( rng q);

      for R be set st R in Car holds R is finite

      proof

        let R be set;

        assume R in Car;

        then ex L be Linear_Combination of B st R = ( Carrier L) & ex i be Element of NAT st i in ( dom p) & ( Sum L) = (p . i);

        hence thesis;

      end;

      hence thesis by A13, A28, FINSET_1: 7;

    end;

    theorem :: RUSUB_4:4

    for V be RealUnitarySpace, A be Subset of V st V is finite-dimensional & A is linearly-independent holds A is finite

    proof

      let V be RealUnitarySpace;

      let A be Subset of V;

      assume that

       A1: V is finite-dimensional and

       A2: A is linearly-independent;

      consider B be Basis of V such that

       A3: A c= B by A2, RUSUB_3: 15;

      B is finite by A1, Th3;

      hence thesis by A3;

    end;

    theorem :: RUSUB_4:5

    

     Th5: for V be RealUnitarySpace, A,B be Basis of V st V is finite-dimensional holds ( card A) = ( card B)

    proof

      let V be RealUnitarySpace;

      let A,B be Basis of V;

      assume V is finite-dimensional;

      then

      reconsider A9 = A, B9 = B as finite Subset of V by Th3;

       the UNITSTR of V = ( Lin B) & A9 is linearly-independent by RUSUB_3:def 2;

      then

       A1: ( card A9) <= ( card B9) by Th2;

       the UNITSTR of V = ( Lin A) & B9 is linearly-independent by RUSUB_3:def 2;

      then ( card B9) <= ( card A9) by Th2;

      hence thesis by A1, XXREAL_0: 1;

    end;

    theorem :: RUSUB_4:6

    

     Th6: for V be RealUnitarySpace holds ( (0). V) is finite-dimensional

    proof

      let V be RealUnitarySpace;

      reconsider V9 = ( (0). V) as strict RealUnitarySpace;

      reconsider I = ( {} the carrier of V9) as finite Subset of V9;

      the carrier of V9 = {( 0. V)} by RUSUB_1:def 2

      .= {( 0. V9)} by RUSUB_1: 4

      .= the carrier of ( (0). V9) by RUSUB_1:def 2;

      then

       A1: V9 = ( (0). V9) by RUSUB_1: 26;

      I is linearly-independent & ( Lin I) = ( (0). V9) by RLVECT_3: 7, RUSUB_3: 3;

      then I is Basis of V9 by A1, RUSUB_3:def 2;

      hence thesis;

    end;

    theorem :: RUSUB_4:7

    

     Th7: for V be RealUnitarySpace, W be Subspace of V st V is finite-dimensional holds W is finite-dimensional

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      set A = the Basis of W;

      consider I be Basis of V such that

       A1: A c= I by RUSUB_3: 24;

      assume V is finite-dimensional;

      then I is finite by Th3;

      hence thesis by A1;

    end;

    registration

      let V be RealUnitarySpace;

      cluster finite-dimensional strict for Subspace of V;

      existence

      proof

        take ( (0). V);

        thus thesis by Th6;

      end;

    end

    registration

      let V be finite-dimensional RealUnitarySpace;

      cluster -> finite-dimensional for Subspace of V;

      correctness by Th7;

    end

    registration

      let V be finite-dimensional RealUnitarySpace;

      cluster strict for Subspace of V;

      existence

      proof

        ( (0). V) is strict finite-dimensional Subspace of V;

        hence thesis;

      end;

    end

    begin

    definition

      let V be RealUnitarySpace;

      assume

       A1: V is finite-dimensional;

      :: RUSUB_4:def2

      func dim V -> Element of NAT means

      : Def2: for I be Basis of V holds it = ( card I);

      existence

      proof

        consider A be finite Subset of V such that

         A2: A is Basis of V by A1;

        consider n be Element of NAT such that

         A3: n = ( card A);

        for I be Basis of V holds ( card I) = n by A1, A2, A3, Th5;

        hence thesis;

      end;

      uniqueness

      proof

        let n,m be Element of NAT ;

        assume that

         A4: for I be Basis of V holds ( card I) = n and

         A5: for I be Basis of V holds ( card I) = m;

        consider A be finite Subset of V such that

         A6: A is Basis of V by A1;

        ( card A) = n by A4, A6;

        hence thesis by A5, A6;

      end;

    end

    theorem :: RUSUB_4:8

    

     Th8: for V be finite-dimensional RealUnitarySpace, W be Subspace of V holds ( dim W) <= ( dim V)

    proof

      let V be finite-dimensional RealUnitarySpace;

      let W be Subspace of V;

      set A = the Basis of W;

      reconsider A as Subset of W;

      A is linearly-independent by RUSUB_3:def 2;

      then

      reconsider B = A as linearly-independent Subset of V by RUSUB_3: 22;

      reconsider A9 = B as finite Subset of V by Th3;

      reconsider V9 = V as RealUnitarySpace;

      set I = the Basis of V9;

      

       A1: ( Lin I) = the UNITSTR of V9 by RUSUB_3:def 2;

      reconsider I as finite Subset of V by Th3;

      

       A2: ( dim V) = ( card I) by Def2;

      ( card A9) <= ( card I) by A1, Th2;

      hence thesis by A2, Def2;

    end;

    theorem :: RUSUB_4:9

    

     Th9: for V be finite-dimensional RealUnitarySpace, A be Subset of V st A is linearly-independent holds ( card A) = ( dim ( Lin A))

    proof

      let V be finite-dimensional RealUnitarySpace;

      let A be Subset of V such that

       A1: A is linearly-independent;

      set W = ( Lin A);

      for x be object st x in A holds x in the carrier of W by STRUCT_0:def 5, RUSUB_3: 2;

      then

      reconsider B = A as linearly-independent Subset of W by A1, RUSUB_3: 23, TARSKI:def 3;

      W = ( Lin B) by RUSUB_3: 28;

      then

      reconsider B as Basis of W by RUSUB_3:def 2;

      ( card B) = ( dim W) by Def2;

      hence thesis;

    end;

    theorem :: RUSUB_4:10

    

     Th10: for V be finite-dimensional RealUnitarySpace holds ( dim V) = ( dim ( (Omega). V))

    proof

      let V be finite-dimensional RealUnitarySpace;

      consider I be finite Subset of V such that

       A1: I is Basis of V by Def1;

      

       A2: ( (Omega). V) = the UNITSTR of V by RUSUB_1:def 3

      .= ( Lin I) by A1, RUSUB_3:def 2;

      ( card I) = ( dim V) & I is linearly-independent by A1, Def2, RUSUB_3:def 2;

      hence thesis by A2, Th9;

    end;

    theorem :: RUSUB_4:11

    for V be finite-dimensional RealUnitarySpace, W be Subspace of V holds ( dim V) = ( dim W) iff ( (Omega). V) = ( (Omega). W)

    proof

      let V be finite-dimensional RealUnitarySpace;

      let W be Subspace of V;

      consider A be finite Subset of V such that

       A1: A is Basis of V by Def1;

      hereby

        set A = the Basis of W;

        consider B be Basis of V such that

         A2: A c= B by RUSUB_3: 24;

        the carrier of W c= the carrier of V by RUSUB_1:def 1;

        then

        reconsider A9 = A as finite Subset of V by Th3, XBOOLE_1: 1;

        reconsider B9 = B as finite Subset of V by Th3;

        assume ( dim V) = ( dim W);

        

        then

         A3: ( card A) = ( dim V) by Def2

        .= ( card B) by Def2;

         A4:

        now

          assume A <> B;

          then A c< B by A2;

          then ( card A9) < ( card B9) by CARD_2: 48;

          hence contradiction by A3;

        end;

        reconsider B as Subset of V;

        reconsider A as Subset of W;

        ( (Omega). V) = the UNITSTR of V by RUSUB_1:def 3

        .= ( Lin B) by RUSUB_3:def 2

        .= ( Lin A) by A4, RUSUB_3: 28

        .= the UNITSTR of W by RUSUB_3:def 2

        .= ( (Omega). W) by RUSUB_1:def 3;

        hence ( (Omega). V) = ( (Omega). W);

      end;

      consider B be finite Subset of W such that

       A5: B is Basis of W by Def1;

      

       A6: A is linearly-independent by A1, RUSUB_3:def 2;

      assume ( (Omega). V) = ( (Omega). W);

      

      then the UNITSTR of V = ( (Omega). W) by RUSUB_1:def 3

      .= the UNITSTR of W by RUSUB_1:def 3;

      

      then

       A7: ( Lin A) = the UNITSTR of W by A1, RUSUB_3:def 2

      .= ( Lin B) by A5, RUSUB_3:def 2;

      

       A8: B is linearly-independent by A5, RUSUB_3:def 2;

      reconsider B as Subset of W;

      reconsider A as Subset of V;

      ( dim V) = ( card A) by A1, Def2

      .= ( dim ( Lin B)) by A6, A7, Th9

      .= ( card B) by A8, Th9

      .= ( dim W) by A5, Def2;

      hence thesis;

    end;

    theorem :: RUSUB_4:12

    

     Th12: for V be finite-dimensional RealUnitarySpace holds ( dim V) = 0 iff ( (Omega). V) = ( (0). V)

    proof

      let V be finite-dimensional RealUnitarySpace;

      consider I be finite Subset of V such that

       A1: I is Basis of V by Def1;

      hereby

        consider I be finite Subset of V such that

         A2: I is Basis of V by Def1;

        assume ( dim V) = 0 ;

        then ( card I) = 0 by A2, Def2;

        then

         A3: I = ( {} the carrier of V);

        ( (Omega). V) = the UNITSTR of V by RUSUB_1:def 3

        .= ( Lin I) by A2, RUSUB_3:def 2

        .= ( (0). V) by A3, RUSUB_3: 3;

        hence ( (Omega). V) = ( (0). V);

      end;

      

       A4: I <> {( 0. V)} by A1, RUSUB_3:def 2, RLVECT_3: 8;

      assume ( (Omega). V) = ( (0). V);

      then the UNITSTR of V = ( (0). V) by RUSUB_1:def 3;

      then ( Lin I) = ( (0). V) by A1, RUSUB_3:def 2;

      then I = {} or I = {( 0. V)} by RUSUB_3: 4;

      hence thesis by A1, A4, Def2, CARD_1: 27;

    end;

    theorem :: RUSUB_4:13

    for V be finite-dimensional RealUnitarySpace holds ( dim V) = 1 iff ex v be VECTOR of V st v <> ( 0. V) & ( (Omega). V) = ( Lin {v})

    proof

      let V be finite-dimensional RealUnitarySpace;

      hereby

        consider I be finite Subset of V such that

         A1: I is Basis of V by Def1;

        assume ( dim V) = 1;

        then ( card I) = 1 by A1, Def2;

        then

        consider v be object such that

         A2: I = {v} by CARD_2: 42;

        v in I by A2, TARSKI:def 1;

        then

        reconsider v as VECTOR of V;

         {v} is linearly-independent by A1, A2, RUSUB_3:def 2;

        then

         A3: v <> ( 0. V) by RLVECT_3: 8;

        ( Lin {v}) = the UNITSTR of V by A1, A2, RUSUB_3:def 2;

        hence ex v be VECTOR of V st v <> ( 0. V) & ( (Omega). V) = ( Lin {v}) by A3, RUSUB_1:def 3;

      end;

      given v be VECTOR of V such that

       A4: v <> ( 0. V) & ( (Omega). V) = ( Lin {v});

       {v} is linearly-independent & ( Lin {v}) = the UNITSTR of V by A4, RLVECT_3: 8, RUSUB_1:def 3;

      then

       A5: {v} is Basis of V by RUSUB_3:def 2;

      ( card {v}) = 1 by CARD_1: 30;

      hence thesis by A5, Def2;

    end;

    theorem :: RUSUB_4:14

    for V be finite-dimensional RealUnitarySpace holds ( dim V) = 2 iff ex u,v be VECTOR of V st u <> v & {u, v} is linearly-independent & ( (Omega). V) = ( Lin {u, v})

    proof

      let V be finite-dimensional RealUnitarySpace;

      hereby

        consider I be finite Subset of V such that

         A1: I is Basis of V by Def1;

        assume ( dim V) = 2;

        then

         A2: ( card I) = 2 by A1, Def2;

        then

        consider u be object such that

         A3: u in I by CARD_1: 27, XBOOLE_0:def 1;

        reconsider u as VECTOR of V by A3;

        now

          assume I c= {u};

          then ( card I) <= ( card {u}) by NAT_1: 43;

          then 2 <= 1 by A2, CARD_1: 30;

          hence contradiction;

        end;

        then

        consider v be object such that

         A4: v in I and

         A5: not v in {u};

        reconsider v as VECTOR of V by A4;

        

         A6: v <> u by A5, TARSKI:def 1;

         A7:

        now

          assume not I c= {u, v};

          then

          consider w be object such that

           A8: w in I and

           A9: not w in {u, v};

          for x be object st x in {u, v, w} holds x in I by A3, A4, A8, ENUMSET1:def 1;

          then {u, v, w} c= I;

          then

           A10: ( card {u, v, w}) <= ( card I) by NAT_1: 43;

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

          then 3 <= 2 by A2, A6, A10, CARD_2: 58;

          hence contradiction;

        end;

        for x be object st x in {u, v} holds x in I by A3, A4, TARSKI:def 2;

        then {u, v} c= I;

        then

         A11: I = {u, v} by A7;

        then

         A12: {u, v} is linearly-independent by A1, RUSUB_3:def 2;

        ( Lin {u, v}) = the UNITSTR of V by A1, A11, RUSUB_3:def 2

        .= ( (Omega). V) by RUSUB_1:def 3;

        hence ex u,v be VECTOR of V st u <> v & {u, v} is linearly-independent & ( (Omega). V) = ( Lin {u, v}) by A6, A12;

      end;

      given u,v be VECTOR of V such that

       A13: u <> v and

       A14: {u, v} is linearly-independent and

       A15: ( (Omega). V) = ( Lin {u, v});

      ( Lin {u, v}) = the UNITSTR of V by A15, RUSUB_1:def 3;

      then

       A16: {u, v} is Basis of V by A14, RUSUB_3:def 2;

      ( card {u, v}) = 2 by A13, CARD_2: 57;

      hence thesis by A16, Def2;

    end;

    theorem :: RUSUB_4:15

    

     Th15: for V be finite-dimensional RealUnitarySpace, W1,W2 be Subspace of V holds (( dim (W1 + W2)) + ( dim (W1 /\ W2))) = (( dim W1) + ( dim W2))

    proof

      let V be finite-dimensional RealUnitarySpace;

      let W1,W2 be Subspace of V;

      reconsider V as RealUnitarySpace;

      reconsider W1, W2 as Subspace of V;

      consider I be finite Subset of (W1 /\ W2) such that

       A1: I is Basis of (W1 /\ W2) by Def1;

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

      then

      consider I2 be Basis of W2 such that

       A2: I c= I2 by A1, RUSUB_3: 24;

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

      then

      consider I1 be Basis of W1 such that

       A3: I c= I1 by A1, RUSUB_3: 24;

      reconsider I2 as finite Subset of W2 by Th3;

      reconsider I1 as finite Subset of W1 by Th3;

       A4:

      now

        I1 is linearly-independent by RUSUB_3:def 2;

        then

        reconsider I19 = I1 as linearly-independent Subset of V by RUSUB_3: 22;

        the carrier of (W1 /\ W2) c= the carrier of V by RUSUB_1:def 1;

        then

        reconsider I9 = I as Subset of V by XBOOLE_1: 1;

        assume not (I1 /\ I2) c= I;

        then

        consider x be object such that

         A5: x in (I1 /\ I2) and

         A6: not x in I;

        x in I1 by A5, XBOOLE_0:def 4;

        then x in ( Lin I1) by RUSUB_3: 2;

        then x in the UNITSTR of W1 by RUSUB_3:def 2;

        then

         A7: x in the carrier of W1;

        

         A8: the carrier of W1 c= the carrier of V by RUSUB_1:def 1;

        then

        reconsider x9 = x as VECTOR of V by A7;

        now

          let y be object;

          the carrier of (W1 /\ W2) c= the carrier of V by RUSUB_1:def 1;

          then

           A9: I c= the carrier of V;

          assume y in (I \/ {x});

          then y in I or y in {x} by XBOOLE_0:def 3;

          then y in the carrier of V or y = x by A9, TARSKI:def 1;

          hence y in the carrier of V by A7, A8;

        end;

        then

        reconsider Ix = (I \/ {x}) as Subset of V by TARSKI:def 3;

        now

          let y be object;

          assume y in (I \/ {x});

          then y in I or y in {x} by XBOOLE_0:def 3;

          then y in I1 or y = x by A3, TARSKI:def 1;

          hence y in I19 by A5, XBOOLE_0:def 4;

        end;

        then

         A10: Ix c= I19;

        x in {x} by TARSKI:def 1;

        then

         A11: x9 in Ix by XBOOLE_0:def 3;

        x in I2 by A5, XBOOLE_0:def 4;

        then x in ( Lin I2) by RUSUB_3: 2;

        then x in the UNITSTR of W2 by RUSUB_3:def 2;

        then x in the carrier of W2;

        then x in (the carrier of W1 /\ the carrier of W2) by A7, XBOOLE_0:def 4;

        then x in the carrier of (W1 /\ W2) by RUSUB_2:def 2;

        then x in the UNITSTR of (W1 /\ W2);

        then

         A12: x in ( Lin I) by A1, RUSUB_3:def 2;

        (Ix \ {x}) = (I \ {x}) by XBOOLE_1: 40

        .= I by A6, ZFMISC_1: 57;

        then not x9 in ( Lin I9) by A10, A11, RLVECT_3: 5, RUSUB_3: 25;

        hence contradiction by A12, RUSUB_3: 28;

      end;

      set A = (I1 \/ I2);

      now

        let v be object;

        

         A13: the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V by RUSUB_1:def 1;

        assume v in A;

        then

         A14: v in I1 or v in I2 by XBOOLE_0:def 3;

        then v in the carrier of W1 or v in the carrier of W2;

        then

        reconsider v9 = v as VECTOR of V by A13;

        v9 in W1 or v9 in W2 by A14;

        then v9 in (W1 + W2) by RUSUB_2: 2;

        hence v in the carrier of (W1 + W2);

      end;

      then

      reconsider A as finite Subset of (W1 + W2) by TARSKI:def 3;

      I c= (I1 /\ I2) by A3, A2, XBOOLE_1: 19;

      then I = (I1 /\ I2) by A4;

      then

       A15: ( card A) = ((( card I1) + ( card I2)) - ( card I)) by CARD_2: 45;

      for L be Linear_Combination of A st ( Sum L) = ( 0. (W1 + W2)) holds ( Carrier L) = {}

      proof

        W1 is Subspace of (W1 + W2) & I1 is linearly-independent by RUSUB_2: 7, RUSUB_3:def 2;

        then

        reconsider I19 = I1 as linearly-independent Subset of (W1 + W2) by RUSUB_3: 22;

        reconsider W29 = W2 as Subspace of (W1 + W2) by RUSUB_2: 7;

        reconsider W19 = W1 as Subspace of (W1 + W2) by RUSUB_2: 7;

        let L be Linear_Combination of A;

        assume

         A16: ( Sum L) = ( 0. (W1 + W2));

        

         A17: I1 misses (( Carrier L) \ I1) by XBOOLE_1: 79;

        set B = (( Carrier L) /\ I1);

        consider F be FinSequence of the carrier of (W1 + W2) such that

         A18: F is one-to-one and

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

         A20: ( Sum L) = ( Sum (L (#) F)) by RLVECT_2:def 8;

        reconsider B as Subset of ( rng F) by A19, XBOOLE_1: 17;

        reconsider F1 = (F - (B ` )), F2 = (F - B) as FinSequence of the carrier of (W1 + W2) by FINSEQ_3: 86;

        consider L1 be Linear_Combination of (W1 + W2) such that

         A21: ( Carrier L1) = (( rng F1) /\ ( Carrier L)) and

         A22: (L1 (#) F1) = (L (#) F1) by RLVECT_5: 7;

        F1 is one-to-one by A18, FINSEQ_3: 87;

        then

         A23: ( Sum (L (#) F1)) = ( Sum L1) by A21, A22, RLVECT_5: 6, XBOOLE_1: 17;

        ( rng F) c= ( rng F);

        then

        reconsider X = ( rng F) as Subset of ( rng F);

        consider L2 be Linear_Combination of (W1 + W2) such that

         A24: ( Carrier L2) = (( rng F2) /\ ( Carrier L)) and

         A25: (L2 (#) F2) = (L (#) F2) by RLVECT_5: 7;

        F2 is one-to-one by A18, FINSEQ_3: 87;

        then

         A26: ( Sum (L (#) F2)) = ( Sum L2) by A24, A25, RLVECT_5: 6, XBOOLE_1: 17;

        (X \ (B ` )) = (X /\ ((B ` ) ` )) by SUBSET_1: 13

        .= B by XBOOLE_1: 28;

        then ( rng F1) = B by FINSEQ_3: 65;

        

        then

         A27: ( Carrier L1) = (I1 /\ (( Carrier L) /\ ( Carrier L))) by A21, XBOOLE_1: 16

        .= (( Carrier L) /\ I1);

        then

        consider K1 be Linear_Combination of W19 such that ( Carrier K1) = ( Carrier L1) and

         A28: ( Sum K1) = ( Sum L1) by RUSUB_3: 20;

        ( rng F2) = (( Carrier L) \ (( Carrier L) /\ I1)) by A19, FINSEQ_3: 65

        .= (( Carrier L) \ I1) by XBOOLE_1: 47;

        then

         A29: ( Carrier L2) = (( Carrier L) \ I1) by A24, XBOOLE_1: 28, XBOOLE_1: 36;

        

        then (( Carrier L1) /\ ( Carrier L2)) = (( Carrier L) /\ (I1 /\ (( Carrier L) \ I1))) by A27, XBOOLE_1: 16

        .= (( Carrier L) /\ {} ) by A17

        .= {} ;

        then

         A30: ( Carrier L1) misses ( Carrier L2);

        

         A31: ( Carrier L) c= (I1 \/ I2) by RLVECT_2:def 6;

        then

         A32: ( Carrier L2) c= I2 by A29, XBOOLE_1: 43;

        ( Carrier L2) c= I2 by A31, A29, XBOOLE_1: 43;

        then

        consider K2 be Linear_Combination of W29 such that ( Carrier K2) = ( Carrier L2) and

         A33: ( Sum K2) = ( Sum L2) by RUSUB_3: 20, XBOOLE_1: 1;

        

         A34: ( Sum K1) in W1;

        ex P be Permutation of ( dom F) st ((F - (B ` )) ^ (F - B)) = (F * P) by FINSEQ_3: 115;

        

        then

         A35: ( 0. (W1 + W2)) = ( Sum (L (#) (F1 ^ F2))) by A16, A20, RLVECT_5: 4

        .= ( Sum ((L (#) F1) ^ (L (#) F2))) by RLVECT_3: 34

        .= (( Sum L1) + ( Sum L2)) by A23, A26, RLVECT_1: 41;

        

        then ( Sum L1) = ( - ( Sum L2)) by RLVECT_1:def 10

        .= ( - ( Sum K2)) by A33, RUSUB_1: 9;

        then ( Sum K1) in W2 by A28;

        then ( Sum K1) in (W1 /\ W2) by A34, RUSUB_2: 3;

        then ( Sum K1) in ( Lin I) by A1, RUSUB_3:def 2;

        then

        consider KI be Linear_Combination of I such that

         A36: ( Sum K1) = ( Sum KI) by RUSUB_3: 1;

        

         A37: ( Carrier L) = (( Carrier L1) \/ ( Carrier L2)) by A27, A29, XBOOLE_1: 51;

         A38:

        now

          assume not ( Carrier L) c= ( Carrier (L1 + L2));

          then

          consider x be object such that

           A39: x in ( Carrier L) and

           A40: not x in ( Carrier (L1 + L2));

          reconsider x as VECTOR of (W1 + W2) by A39;

          

           A41: 0 = ((L1 + L2) . x) by A40, RLVECT_2: 19

          .= ((L1 . x) + (L2 . x)) by RLVECT_2:def 10;

          per cases by A37, A39, XBOOLE_0:def 3;

            suppose

             A42: x in ( Carrier L1);

            then not x in ( Carrier L2) by A30, XBOOLE_0: 3;

            then

             A43: (L2 . x) = 0 by RLVECT_2: 19;

            ex v be VECTOR of (W1 + W2) st x = v & (L1 . v) <> 0 by A42, RLVECT_5: 3;

            hence contradiction by A41, A43;

          end;

            suppose

             A44: x in ( Carrier L2);

            then not x in ( Carrier L1) by A30, XBOOLE_0: 3;

            then

             A45: (L1 . x) = 0 by RLVECT_2: 19;

            ex v be VECTOR of (W1 + W2) st x = v & (L2 . v) <> 0 by A44, RLVECT_5: 3;

            hence contradiction by A41, A45;

          end;

        end;

        

         A46: (I \/ I2) = I2 by A2, XBOOLE_1: 12;

        

         A47: I2 is linearly-independent by RUSUB_3:def 2;

        

         A48: ( Carrier L1) c= I1 by A27, XBOOLE_1: 17;

        (W1 /\ W2) is Subspace of (W1 + W2) by RUSUB_2: 22;

        then

        consider LI be Linear_Combination of (W1 + W2) such that

         A49: ( Carrier LI) = ( Carrier KI) and

         A50: ( Sum LI) = ( Sum KI) by RUSUB_3: 19;

        ( Carrier LI) c= I by A49, RLVECT_2:def 6;

        then ( Carrier LI) c= I19 by A3;

        then

         A51: LI = L1 by A48, A28, A36, A50, RLVECT_5: 1;

        ( Carrier LI) c= I by A49, RLVECT_2:def 6;

        then ( Carrier (LI + L2)) c= (( Carrier LI) \/ ( Carrier L2)) & (( Carrier LI) \/ ( Carrier L2)) c= I2 by A46, A32, RLVECT_2: 37, XBOOLE_1: 13;

        then

         A52: ( Carrier (LI + L2)) c= I2;

        W2 is Subspace of (W1 + W2) by RUSUB_2: 7;

        then

        consider K be Linear_Combination of W2 such that

         A53: ( Carrier K) = ( Carrier (LI + L2)) and

         A54: ( Sum K) = ( Sum (LI + L2)) by A52, RUSUB_3: 20, XBOOLE_1: 1;

        reconsider K as Linear_Combination of I2 by A52, A53, RLVECT_2:def 6;

        ( 0. W2) = (( Sum LI) + ( Sum L2)) by A28, A35, A36, A50, RUSUB_1: 5

        .= ( Sum K) by A54, RLVECT_3: 1;

        then {} = ( Carrier (L1 + L2)) by A53, A51, A47, RLVECT_3:def 1;

        hence thesis by A38;

      end;

      then

       A55: A is linearly-independent by RLVECT_3:def 1;

      the carrier of (W1 + W2) c= the carrier of V by RUSUB_1:def 1;

      then

      reconsider A9 = A as Subset of V by XBOOLE_1: 1;

      

       A56: ( card I2) = ( dim W2) by Def2;

      now

        let x be object;

        assume x in the carrier of (W1 + W2);

        then x in (W1 + W2);

        then

        consider w1,w2 be VECTOR of V such that

         A57: w1 in W1 and

         A58: w2 in W2 and

         A59: x = (w1 + w2) by RUSUB_2: 1;

        reconsider w1 as VECTOR of W1 by A57;

        w1 in ( Lin I1) by RUSUB_3: 21;

        then

        consider K1 be Linear_Combination of I1 such that

         A60: w1 = ( Sum K1) by RUSUB_3: 1;

        reconsider w2 as VECTOR of W2 by A58;

        w2 in ( Lin I2) by RUSUB_3: 21;

        then

        consider K2 be Linear_Combination of I2 such that

         A61: w2 = ( Sum K2) by RUSUB_3: 1;

        consider L2 be Linear_Combination of V such that

         A62: ( Carrier L2) = ( Carrier K2) and

         A63: ( Sum L2) = ( Sum K2) by RUSUB_3: 19;

        

         A64: ( Carrier L2) c= I2 by A62, RLVECT_2:def 6;

        consider L1 be Linear_Combination of V such that

         A65: ( Carrier L1) = ( Carrier K1) and

         A66: ( Sum L1) = ( Sum K1) by RUSUB_3: 19;

        set L = (L1 + L2);

        ( Carrier L1) c= I1 by A65, RLVECT_2:def 6;

        then ( Carrier L) c= (( Carrier L1) \/ ( Carrier L2)) & (( Carrier L1) \/ ( Carrier L2)) c= (I1 \/ I2) by A64, RLVECT_2: 37, XBOOLE_1: 13;

        then ( Carrier L) c= (I1 \/ I2);

        then

        reconsider L as Linear_Combination of A9 by RLVECT_2:def 6;

        x = ( Sum L) by A59, A60, A66, A61, A63, RLVECT_3: 1;

        then x in ( Lin A9) by RUSUB_3: 1;

        hence x in the carrier of ( Lin A9);

      end;

      then the carrier of (W1 + W2) c= the carrier of ( Lin A9);

      then ( Lin A9) = ( Lin A) & (W1 + W2) is Subspace of ( Lin A9) by RUSUB_1: 22, RUSUB_3: 28;

      then ( Lin A) = (W1 + W2) by RUSUB_1: 20;

      then

       A67: A is Basis of (W1 + W2) by A55, RUSUB_3:def 2;

      ( card I) = ( dim (W1 /\ W2)) by A1, Def2;

      

      then (( dim (W1 + W2)) + ( dim (W1 /\ W2))) = (((( card I1) + ( card I2)) + ( - ( card I))) + ( card I)) by A15, A67, Def2

      .= (( dim W1) + ( dim W2)) by A56, Def2;

      hence thesis;

    end;

    theorem :: RUSUB_4:16

    for V be finite-dimensional RealUnitarySpace, W1,W2 be Subspace of V holds ( dim (W1 /\ W2)) >= ((( dim W1) + ( dim W2)) - ( dim V))

    proof

      let V be finite-dimensional RealUnitarySpace;

      let W1,W2 be Subspace of V;

      

       A1: ( dim (W1 + W2)) <= ( dim V) & (( dim V) + (( dim (W1 /\ W2)) - ( dim V))) = ( dim (W1 /\ W2)) by Th8;

      ((( dim W1) + ( dim W2)) - ( dim V)) = ((( dim (W1 + W2)) + ( dim (W1 /\ W2))) - ( dim V)) by Th15

      .= (( dim (W1 + W2)) + (( dim (W1 /\ W2)) - ( dim V)));

      hence thesis by A1, XREAL_1: 6;

    end;

    theorem :: RUSUB_4:17

    for V be finite-dimensional RealUnitarySpace, W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds ( dim V) = (( dim W1) + ( dim W2))

    proof

      let V be finite-dimensional RealUnitarySpace;

      let W1,W2 be Subspace of V;

      assume

       A1: V is_the_direct_sum_of (W1,W2);

      then

       A2: the UNITSTR of V = (W1 + W2) by RUSUB_2:def 4;

      (W1 /\ W2) = ( (0). V) by A1, RUSUB_2:def 4;

      

      then ( (Omega). (W1 /\ W2)) = ( (0). V) by RUSUB_1:def 3

      .= ( (0). (W1 /\ W2)) by RUSUB_1: 30;

      then ( dim (W1 /\ W2)) = 0 by Th12;

      

      then (( dim W1) + ( dim W2)) = (( dim (W1 + W2)) + 0 ) by Th15

      .= ( dim ( (Omega). V)) by A2, RUSUB_1:def 3

      .= ( dim V) by Th10;

      hence thesis;

    end;

    begin

    

     Lm2: for V be finite-dimensional RealUnitarySpace, n be Element of NAT st n <= ( dim V) holds ex W be strict Subspace of V st ( dim W) = n

    proof

      let V be finite-dimensional RealUnitarySpace;

      let n be Element of NAT ;

      consider I be finite Subset of V such that

       A1: I is Basis of V by Def1;

      assume n <= ( dim V);

      then n <= ( card I) by A1, Def2;

      then

      consider A be finite Subset of I such that

       A2: ( card A) = n by FINSEQ_4: 72;

      reconsider A as Subset of V by XBOOLE_1: 1;

      reconsider W = ( Lin A) as strict finite-dimensional Subspace of V;

      I is linearly-independent by A1, RUSUB_3:def 2;

      then ( dim W) = n by A2, Th9, RLVECT_3: 5;

      hence thesis;

    end;

    theorem :: RUSUB_4:18

    for V be finite-dimensional RealUnitarySpace, W be Subspace of V, n be Element of NAT holds n <= ( dim V) iff ex W be strict Subspace of V st ( dim W) = n by Lm2, Th8;

    definition

      let V be finite-dimensional RealUnitarySpace, n be Element of NAT ;

      :: RUSUB_4:def3

      func n Subspaces_of V -> set means

      : Def3: for x be object holds x in it iff ex W be strict Subspace of V st W = x & ( dim W) = n;

      existence

      proof

        set S = { ( Lin A) where A be Subset of V : A is linearly-independent & ( card A) = n };

        take S;

        for x be object holds x in S iff ex W be strict Subspace of V st W = x & ( dim W) = n

        proof

          let x be object;

          hereby

            assume x in S;

            then

             A1: ex A be Subset of V st x = ( Lin A) & A is linearly-independent & ( card A) = n;

            then

            reconsider W = x as strict Subspace of V;

            ( dim W) = n by A1, Th9;

            hence ex W be strict Subspace of V st W = x & ( dim W) = n;

          end;

          given W be strict Subspace of V such that

           A2: W = x and

           A3: ( dim W) = n;

          consider A be finite Subset of W such that

           A4: A is Basis of W by Def1;

          reconsider A as Subset of W;

          A is linearly-independent by A4, RUSUB_3:def 2;

          then

          reconsider B = A as linearly-independent Subset of V by RUSUB_3: 22;

          

           A5: x = ( Lin A) by A2, A4, RUSUB_3:def 2

          .= ( Lin B) by RUSUB_3: 28;

          then ( card B) = n by A2, A3, Th9;

          hence thesis by A5;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        defpred P[ object] means ex W be strict Subspace of V st W = $1 & ( dim W) = n;

        for X1,X2 be set st (for x be object holds x in X1 iff P[x]) & (for x be object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;

        hence thesis;

      end;

    end

    theorem :: RUSUB_4:19

    for V be finite-dimensional RealUnitarySpace, n be Element of NAT st n <= ( dim V) holds (n Subspaces_of V) is non empty

    proof

      let V be finite-dimensional RealUnitarySpace;

      let n be Element of NAT ;

      assume n <= ( dim V);

      then ex W be strict Subspace of V st ( dim W) = n by Lm2;

      hence thesis by Def3;

    end;

    theorem :: RUSUB_4:20

    for V be finite-dimensional RealUnitarySpace, n be Element of NAT st ( dim V) < n holds (n Subspaces_of V) = {}

    proof

      let V be finite-dimensional RealUnitarySpace;

      let n be Element of NAT ;

      assume that

       A1: ( dim V) < n and

       A2: (n Subspaces_of V) <> {} ;

      consider x be object such that

       A3: x in (n Subspaces_of V) by A2, XBOOLE_0:def 1;

      ex W be strict Subspace of V st W = x & ( dim W) = n by A3, Def3;

      hence contradiction by A1, Th8;

    end;

    theorem :: RUSUB_4:21

    for V be finite-dimensional RealUnitarySpace, W be Subspace of V, n be Element of NAT holds (n Subspaces_of W) c= (n Subspaces_of V)

    proof

      let V be finite-dimensional RealUnitarySpace;

      let W be Subspace of V;

      let n be Element of NAT ;

      let x be object;

      assume x in (n Subspaces_of W);

      then

      consider W1 be strict Subspace of W such that

       A1: W1 = x and

       A2: ( dim W1) = n by Def3;

      reconsider W1 as strict Subspace of V by RUSUB_1: 21;

      W1 in (n Subspaces_of V) by A2, Def3;

      hence thesis by A1;

    end;

    begin

    definition

      let V be non empty RLSStruct, S be Subset of V;

      :: RUSUB_4:def4

      attr S is Affine means

      : Def4: for x,y be VECTOR of V, a be Real st x in S & y in S holds (((1 - a) * x) + (a * y)) in S;

    end

    theorem :: RUSUB_4:22

    for V be non empty RLSStruct holds ( [#] V) is Affine & ( {} V) is Affine;

    theorem :: RUSUB_4:23

    for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, v be VECTOR of V holds {v} is Affine

    proof

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

      let v be VECTOR of V;

      for x,y be VECTOR of V, a be Real st x in {v} & y in {v} holds (((1 - a) * x) + (a * y)) in {v}

      proof

        let x,y be VECTOR of V;

        let a be Real;

        assume x in {v} & y in {v};

        then x = v & y = v by TARSKI:def 1;

        

        then (((1 - a) * x) + (a * y)) = (((1 - a) + a) * v) by RLVECT_1:def 6

        .= v by RLVECT_1:def 8;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis;

    end;

    registration

      let V be non empty RLSStruct;

      cluster non empty Affine for Subset of V;

      existence

      proof

        take ( [#] V);

        thus thesis;

      end;

      cluster empty Affine for Subset of V;

      existence

      proof

        take ( {} V);

        thus thesis;

      end;

    end

    definition

      let V be RealLinearSpace, W be Subspace of V;

      :: RUSUB_4:def5

      func Up (W) -> non empty Subset of V equals the carrier of W;

      coherence by RLSUB_1:def 2;

    end

    definition

      let V be RealUnitarySpace, W be Subspace of V;

      :: RUSUB_4:def6

      func Up (W) -> non empty Subset of V equals the carrier of W;

      coherence by RUSUB_1:def 1;

    end

    theorem :: RUSUB_4:24

    for V be RealLinearSpace, W be Subspace of V holds ( Up W) is Affine & ( 0. V) in the carrier of W

    proof

      let V be RealLinearSpace;

      let W be Subspace of V;

      for x,y be VECTOR of V, a be Real st x in ( Up W) & y in ( Up W) holds (((1 - a) * x) + (a * y)) in ( Up W)

      proof

        let x,y be VECTOR of V;

        let a be Real;

        assume that

         A1: x in ( Up W) and

         A2: y in ( Up W);

        reconsider aa = a as Real;

        y in W by A2;

        then

         A3: (aa * y) in W by RLSUB_1: 21;

        x in W by A1;

        then ((1 - aa) * x) in W by RLSUB_1: 21;

        then (((1 - a) * x) + (a * y)) in W by A3, RLSUB_1: 20;

        hence thesis;

      end;

      hence ( Up W) is Affine;

      ( 0. V) in W by RLSUB_1: 17;

      hence thesis;

    end;

    theorem :: RUSUB_4:25

    

     Th25: for V be RealLinearSpace, A be Affine Subset of V st ( 0. V) in A holds for x be VECTOR of V, a be Real st x in A holds (a * x) in A

    proof

      let V be RealLinearSpace;

      let A be Affine Subset of V;

      assume

       A1: ( 0. V) in A;

      for x be VECTOR of V, a be Real st x in A holds (a * x) in A

      proof

        let x be VECTOR of V;

        let a be Real;

        assume x in A;

        then (((1 - a) * ( 0. V)) + (a * x)) in A by A1, Def4;

        then (( 0. V) + (a * x)) in A;

        hence thesis;

      end;

      hence thesis;

    end;

    definition

      let V be non empty RLSStruct, S be non empty Subset of V;

      :: RUSUB_4:def7

      attr S is Subspace-like means ( 0. V) in S & for x,y be Element of V, a be Real st x in S & y in S holds (x + y) in S & (a * x) in S;

    end

    theorem :: RUSUB_4:26

    

     Th26: for V be RealLinearSpace, A be non empty Affine Subset of V st ( 0. V) in A holds A is Subspace-like & A = the carrier of ( Lin A)

    proof

      let V be RealLinearSpace;

      let A be non empty Affine Subset of V;

      assume

       A1: ( 0. V) in A;

      

       A2: for x,y be Element of V, a be Real st x in A & y in A holds (x + y) in A & (a * x) in A

      proof

        let x,y be Element of V;

        let a be Real;

        assume that

         A3: x in A and

         A4: y in A;

        reconsider x, y as VECTOR of V;

        

         A5: (2 * (((1 - (1 / 2)) * x) + ((1 / 2) * y))) = ((2 * ((1 - (1 / 2)) * x)) + (2 * ((1 / 2) * y))) by RLVECT_1:def 5

        .= (((2 * (1 - (1 / 2))) * x) + (2 * ((1 / 2) * y))) by RLVECT_1:def 7

        .= (((2 - 1) * x) + ((2 * (1 / 2)) * y)) by RLVECT_1:def 7

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

        .= (x + y) by RLVECT_1:def 8;

        (((1 - (1 / 2)) * x) + ((1 / 2) * y)) in A by A3, A4, Def4;

        hence thesis by A1, A3, A5, Th25;

      end;

      hence A is Subspace-like by A1;

      for x be object st x in the carrier of ( Lin A) holds x in A

      proof

        let x be object;

        assume x in the carrier of ( Lin A);

        then x in ( Lin A);

        then

         A6: ex l be Linear_Combination of A st x = ( Sum l) by RLVECT_3: 14;

        (for v,u be VECTOR of V st v in A & u in A holds (v + u) in A) & for a be Real, v be VECTOR of V st v in A holds (a * v) in A by A2;

        then A is linearly-closed by RLSUB_1:def 1;

        hence thesis by A6, RLVECT_2: 29;

      end;

      then

       A7: the carrier of ( Lin A) c= A;

      for x be object st x in A holds x in the carrier of ( Lin A) by RLVECT_3: 15, STRUCT_0:def 5;

      then A c= the carrier of ( Lin A);

      hence thesis by A7;

    end;

    theorem :: RUSUB_4:27

    for V be RealLinearSpace, W be Subspace of V holds ( Up W) is Subspace-like

    proof

      let V be RealLinearSpace;

      let W be Subspace of V;

      ( 0. V) in W by RLSUB_1: 17;

      hence ( 0. V) in ( Up W);

      thus for x,y be Element of V, a be Real st x in ( Up W) & y in ( Up W) holds (x + y) in ( Up W) & (a * x) in ( Up W)

      proof

        let x,y be Element of V;

        let a be Real;

        assume that

         A1: x in ( Up W) and

         A2: y in ( Up W);

        reconsider x, y as Element of V;

        reconsider aa = a as Real;

        

         A3: x in W by A1;

        then

         A4: (aa * x) in W by RLSUB_1: 21;

        y in W by A2;

        then (x + y) in W by A3, RLSUB_1: 20;

        hence thesis by A4;

      end;

    end;

    theorem :: RUSUB_4:28

    for V be RealUnitarySpace, A be non empty Affine Subset of V st ( 0. V) in A holds A = the carrier of ( Lin A)

    proof

      let V be RealUnitarySpace;

      let A be non empty Affine Subset of V;

      assume ( 0. V) in A;

      then

       A1: A is Subspace-like by Th26;

      for x be object st x in the carrier of ( Lin A) holds x in A

      proof

        let x be object;

        assume x in the carrier of ( Lin A);

        then x in ( Lin A);

        then

         A2: ex l be Linear_Combination of A st x = ( Sum l) by RUSUB_3: 1;

        (for v,u be VECTOR of V st v in A & u in A holds (v + u) in A) & for a be Real, v be VECTOR of V st v in A holds (a * v) in A by A1;

        then A is linearly-closed by RLSUB_1:def 1;

        hence thesis by A2, RLVECT_2: 29;

      end;

      then

       A3: the carrier of ( Lin A) c= A;

      for x be object st x in A holds x in the carrier of ( Lin A) by RUSUB_3: 2, STRUCT_0:def 5;

      then A c= the carrier of ( Lin A);

      hence thesis by A3;

    end;

    theorem :: RUSUB_4:29

    for V be RealUnitarySpace, W be Subspace of V holds ( Up W) is Subspace-like

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      ( 0. V) in W by RUSUB_1: 11;

      hence ( 0. V) in ( Up W);

      thus for x,y be Element of V, a be Real st x in ( Up W) & y in ( Up W) holds (x + y) in ( Up W) & (a * x) in ( Up W)

      proof

        let x,y be Element of V;

        let a be Real;

        assume that

         A1: x in ( Up W) and

         A2: y in ( Up W);

        reconsider x, y as Element of V;

        

         A3: x in W by A1;

        then

         A4: (a * x) in W by RUSUB_1: 15;

        y in W by A2;

        then (x + y) in W by A3, RUSUB_1: 14;

        hence thesis by A4;

      end;

    end;

    definition

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

      :: RUSUB_4:def8

      func v + M -> Subset of V equals { (v + u) where u be Element of V : u in M };

      coherence

      proof

        set Y = { (v + u) where u be Element of V : u in M };

        defpred P[ object] means ex u be Element of V st $1 = (v + u) & u in M;

        consider X be set such that

         A1: for x be object holds x in X iff x in the carrier of V & P[x] from XBOOLE_0:sch 1;

        X c= the carrier of V by A1;

        then

        reconsider X as Subset of V;

        reconsider X as Subset of V;

        

         A2: Y c= X

        proof

          let x be object;

          assume x in Y;

          then ex u be Element of V st x = (v + u) & u in M;

          hence thesis by A1;

        end;

        X c= Y

        proof

          let x be object;

          assume x in X;

          then ex u be Element of V st x = (v + u) & u in M by A1;

          hence thesis;

        end;

        hence thesis by A2, XBOOLE_0:def 10;

      end;

    end

    theorem :: RUSUB_4:30

    for V be RealLinearSpace, W be strict Subspace of V, M be Subset of V, v be VECTOR of V st ( Up W) = M holds (v + W) = (v + M)

    proof

      let V be RealLinearSpace;

      let W be strict Subspace of V;

      let M be Subset of V;

      let v be VECTOR of V;

      assume

       A1: ( Up W) = M;

      for x be object st x in (v + M) holds x in (v + W)

      proof

        let x be object;

        assume x in (v + M);

        then

        consider u be Element of V such that

         A2: x = (v + u) and

         A3: u in M;

        u in W by A1, A3;

        then x in { (v + u9) where u9 be VECTOR of V : u9 in W } by A2;

        hence thesis by RLSUB_1:def 5;

      end;

      then

       A4: (v + M) c= (v + W);

      for x be object st x in (v + W) holds x in (v + M)

      proof

        let x be object;

        assume x in (v + W);

        then x in { (v + u) where u be VECTOR of V : u in W } by RLSUB_1:def 5;

        then

        consider u be VECTOR of V such that

         A5: x = (v + u) and

         A6: u in W;

        u in M by A1, A6;

        hence thesis by A5;

      end;

      then (v + W) c= (v + M);

      hence thesis by A4;

    end;

    theorem :: RUSUB_4:31

    

     Th31: for V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M be Affine Subset of V, v be VECTOR of V holds (v + M) is Affine

    proof

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

      let M be Affine Subset of V;

      let v be VECTOR of V;

      for x,y be VECTOR of V, a be Real st x in (v + M) & y in (v + M) holds (((1 - a) * x) + (a * y)) in (v + M)

      proof

        let x,y be VECTOR of V;

        let a be Real;

        assume that

         A1: x in (v + M) and

         A2: y in (v + M);

        consider x9 be Element of V such that

         A3: x = (v + x9) and

         A4: x9 in M by A1;

        consider y9 be Element of V such that

         A5: y = (v + y9) and

         A6: y9 in M by A2;

        

         A7: (((1 - a) * x) + (a * y)) = ((((1 - a) * v) + ((1 - a) * x9)) + (a * (v + y9))) by A3, A5, RLVECT_1:def 5

        .= ((((1 - a) * v) + ((1 - a) * x9)) + ((a * v) + (a * y9))) by RLVECT_1:def 5

        .= (((((1 - a) * v) + ((1 - a) * x9)) + (a * v)) + (a * y9)) by RLVECT_1:def 3

        .= ((((1 - a) * x9) + (((1 - a) * v) + (a * v))) + (a * y9)) by RLVECT_1:def 3

        .= ((((1 - a) * x9) + (((1 - a) + a) * v)) + (a * y9)) by RLVECT_1:def 6

        .= ((((1 - a) * x9) + v) + (a * y9)) by RLVECT_1:def 8

        .= (v + (((1 - a) * x9) + (a * y9))) by RLVECT_1:def 3;

        (((1 - a) * x9) + (a * y9)) in M by A4, A6, Def4;

        hence thesis by A7;

      end;

      hence thesis;

    end;

    theorem :: RUSUB_4:32

    for V be RealUnitarySpace, W be strict Subspace of V, M be Subset of V, v be VECTOR of V st ( Up W) = M holds (v + W) = (v + M)

    proof

      let V be RealUnitarySpace;

      let W be strict Subspace of V;

      let M be Subset of V;

      let v be VECTOR of V;

      assume

       A1: ( Up W) = M;

      for x be object st x in (v + M) holds x in (v + W)

      proof

        let x be object;

        assume x in (v + M);

        then

        consider u be Element of V such that

         A2: x = (v + u) and

         A3: u in M;

        u in W by A1, A3;

        then x in { (v + u9) where u9 be VECTOR of V : u9 in W } by A2;

        hence thesis by RUSUB_1:def 4;

      end;

      then

       A4: (v + M) c= (v + W);

      for x be object st x in (v + W) holds x in (v + M)

      proof

        let x be object;

        assume x in (v + W);

        then x in { (v + u) where u be VECTOR of V : u in W } by RUSUB_1:def 4;

        then

        consider u be VECTOR of V such that

         A5: x = (v + u) and

         A6: u in W;

        u in M by A1, A6;

        hence thesis by A5;

      end;

      then (v + W) c= (v + M);

      hence thesis by A4;

    end;

    definition

      let V be non empty addLoopStr, M,N be Subset of V;

      :: RUSUB_4:def9

      func M + N -> Subset of V equals { (u + v) where u,v be Element of V : u in M & v in N };

      coherence

      proof

        defpred P[ set, set] means $1 in M & $2 in N;

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

        { F(u,v) where u,v be Element of V : P[u, v] } is Subset of V from DOMAIN_1:sch 9;

        hence thesis;

      end;

    end

    definition

      let V be Abelian non empty addLoopStr, M,N be Subset of V;

      :: original: +

      redefine

      func M + N;

      commutativity

      proof

        let M,N be Subset of V;

        for x be object st x in (M + N) holds x in (N + M)

        proof

          let x be object;

          assume x in (M + N);

          then ex u1,v1 be Element of V st x = (u1 + v1) & u1 in M & v1 in N;

          hence thesis;

        end;

        then

         A1: (M + N) c= (N + M);

        for x be object st x in (N + M) holds x in (M + N)

        proof

          let x be object;

          assume x in (N + M);

          then ex u1,v1 be Element of V st x = (u1 + v1) & u1 in N & v1 in M;

          hence thesis;

        end;

        then (N + M) c= (M + N);

        hence thesis by A1;

      end;

    end

    theorem :: RUSUB_4:33

    

     Th33: for V be non empty addLoopStr, M be Subset of V, v be Element of V holds ( {v} + M) = (v + M)

    proof

      let V be non empty addLoopStr;

      let M be Subset of V;

      let v be Element of V;

      for x be object st x in (v + M) holds x in ( {v} + M)

      proof

        let x be object;

        assume x in (v + M);

        then

         A1: ex u be Element of V st x = (v + u) & u in M;

        v in {v} by TARSKI:def 1;

        hence thesis by A1;

      end;

      then

       A2: (v + M) c= ( {v} + M);

      for x be object st x in ( {v} + M) holds x in (v + M)

      proof

        let x be object;

        assume x in ( {v} + M);

        then

        consider v1,u1 be Element of V such that

         A3: x = (v1 + u1) and

         A4: v1 in {v} and

         A5: u1 in M;

        v1 = v by A4, TARSKI:def 1;

        hence thesis by A3, A5;

      end;

      then ( {v} + M) c= (v + M);

      hence thesis by A2;

    end;

    theorem :: RUSUB_4:34

    for V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M be Affine Subset of V, v be VECTOR of V holds ( {v} + M) is Affine

    proof

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

      let M be Affine Subset of V;

      let v be VECTOR of V;

      ( {v} + M) = (v + M) by Th33;

      hence thesis by Th31;

    end;

    theorem :: RUSUB_4:35

    for V be non empty RLSStruct, M,N be Affine Subset of V holds (M /\ N) is Affine

    proof

      let V be non empty RLSStruct;

      let M,N be Affine Subset of V;

      for x,y be VECTOR of V, a be Real st x in (M /\ N) & y in (M /\ N) holds (((1 - a) * x) + (a * y)) in (M /\ N)

      proof

        let x,y be VECTOR of V;

        let a be Real;

        assume

         A1: x in (M /\ N) & y in (M /\ N);

        then x in N & y in N by XBOOLE_0:def 4;

        then

         A2: (((1 - a) * x) + (a * y)) in N by Def4;

        x in M & y in M by A1, XBOOLE_0:def 4;

        then (((1 - a) * x) + (a * y)) in M by Def4;

        hence thesis by A2, XBOOLE_0:def 4;

      end;

      hence thesis;

    end;

    theorem :: RUSUB_4:36

    for V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M,N be Affine Subset of V holds (M + N) is Affine

    proof

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

      let M,N be Affine Subset of V;

      for x,y be VECTOR of V, a be Real st x in (M + N) & y in (M + N) holds (((1 - a) * x) + (a * y)) in (M + N)

      proof

        let x,y be VECTOR of V;

        let a be Real;

        assume that

         A1: x in (M + N) and

         A2: y in (M + N);

        consider u1,v1 be Element of V such that

         A3: x = (u1 + v1) and

         A4: u1 in M & v1 in N by A1;

        consider u2,v2 be Element of V such that

         A5: y = (u2 + v2) and

         A6: u2 in M & v2 in N by A2;

        

         A7: (((1 - a) * x) + (a * y)) = ((((1 - a) * u1) + ((1 - a) * v1)) + (a * (u2 + v2))) by A3, A5, RLVECT_1:def 5

        .= ((((1 - a) * u1) + ((1 - a) * v1)) + ((a * u2) + (a * v2))) by RLVECT_1:def 5

        .= (((((1 - a) * u1) + ((1 - a) * v1)) + (a * u2)) + (a * v2)) by RLVECT_1:def 3

        .= ((((1 - a) * v1) + (((1 - a) * u1) + (a * u2))) + (a * v2)) by RLVECT_1:def 3

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

        (((1 - a) * u1) + (a * u2)) in M & (((1 - a) * v1) + (a * v2)) in N by A4, A6, Def4;

        hence thesis by A7;

      end;

      hence thesis;

    end;