rusub_3.miz



    begin

    definition

      let V be RealUnitarySpace;

      let A be Subset of V;

      :: RUSUB_3:def1

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

      : Def1: the carrier of it = the set of all ( Sum l) where l be Linear_Combination of A;

      existence

      proof

        set A1 = the set of all ( Sum l) where l be Linear_Combination of A;

        A1 c= the carrier of V

        proof

          let x be object;

          assume x in A1;

          then ex l be Linear_Combination of A 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 be VECTOR of V st v in A1 & u in A1 holds (v + u) in A1

          proof

            let v,u be VECTOR of V;

            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, RLVECT_3: 1;

            hence thesis;

          end;

          let a be Real;

          let v be VECTOR of V;

          assume v in A1;

          then

          consider l be Linear_Combination of A 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, RLVECT_3: 2;

          hence thesis;

        end;

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

        then ( 0. V) in A1;

        hence thesis by A1, RUSUB_1: 29;

      end;

      uniqueness by RUSUB_1: 24;

    end

    theorem :: RUSUB_3:1

    

     Th1: for V be RealUnitarySpace, A be Subset of V, x be object holds x in ( Lin A) iff ex l be Linear_Combination of A st x = ( Sum l)

    proof

      let V be RealUnitarySpace;

      let A be Subset of V;

      let x be object;

      thus x in ( Lin A) implies ex l be Linear_Combination of A 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) where l be Linear_Combination of A by Def1;

        hence thesis;

      end;

      given k be Linear_Combination of A such that

       A1: x = ( Sum k);

      x in the set of all ( Sum l) where l be Linear_Combination of A by A1;

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

      hence thesis by STRUCT_0:def 5;

    end;

    reconsider jj = 1, zz = ( In ( 0 , REAL )) as Element of REAL by XREAL_0:def 1;

    theorem :: RUSUB_3:2

    

     Th2: for V be RealUnitarySpace, A be Subset of V, x be set st x in A holds x in ( Lin A)

    proof

      deffunc F( set) = zz;

      let V be RealUnitarySpace;

      let A be Subset of V;

      let x be set;

      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 be VECTOR of V st u <> v holds (f . u) = F(u) from FUNCT_2:sch 6;

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

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

      proof

        take T = {v};

        let u be VECTOR of V;

        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 be VECTOR of V 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 Th1;

    end;

    

     Lm1: for V be RealUnitarySpace, x be object holds x in ( (0). V) iff x = ( 0. V)

    proof

      let V be RealUnitarySpace;

      let x be object;

      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 RUSUB_1:def 2;

        hence thesis by TARSKI:def 1;

      end;

      thus thesis by RUSUB_1: 11;

    end;

    theorem :: RUSUB_3:3

    for V be RealUnitarySpace holds ( Lin ( {} the carrier of V)) = ( (0). V)

    proof

      let V be RealUnitarySpace;

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

      now

        let v be VECTOR of 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) where l0 be Linear_Combination of ( {} the carrier of V) by Def1;

          then ex l0 be Linear_Combination of ( {} the carrier of V) st v = ( Sum l0) by A1;

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

          hence thesis by Lm1;

        end;

        assume v in ( (0). V);

        then v = ( 0. V) by Lm1;

        hence v in A by RUSUB_1: 11;

      end;

      hence thesis by RUSUB_1: 25;

    end;

    theorem :: RUSUB_3:4

    for V be RealUnitarySpace, A be Subset of V st ( Lin A) = ( (0). V) holds A = {} or A = {( 0. V)}

    proof

      let V be RealUnitarySpace;

      let A be Subset of V;

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

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

        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, Th2;

      hence thesis by A1, A3, Lm1;

    end;

    theorem :: RUSUB_3:5

    

     Th5: for V be RealUnitarySpace, W be strict Subspace of V, A be Subset of V st A = the carrier of W holds ( Lin A) = W

    proof

      let V be RealUnitarySpace;

      let W be strict Subspace of V;

      let A be Subset of V;

      assume

       A1: A = the carrier of W;

      now

        let v be VECTOR of V;

        thus v in ( Lin A) implies v in W

        proof

          assume v in ( Lin A);

          then

           A2: ex l be Linear_Combination of A st v = ( Sum l) by Th1;

          A is linearly-closed by A1, RUSUB_1: 28;

          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, Th2;

      end;

      hence thesis by RUSUB_1: 25;

    end;

    theorem :: RUSUB_3:6

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

    proof

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

      assume A = the carrier of V;

      then A = the carrier of ( (Omega). V) by RUSUB_1:def 3;

      

      hence ( Lin A) = ( (Omega). V) by Th5

      .= V by RUSUB_1:def 3;

    end;

    

     Lm2: for V be RealUnitarySpace, W1,W2,W3 be Subspace of V st W1 is Subspace of W3 holds (W1 /\ W2) is Subspace of W3

    proof

      let V be RealUnitarySpace;

      let W1,W2,W3 be Subspace of V;

      

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

      assume W1 is Subspace of W3;

      hence thesis by A1, RUSUB_1: 21;

    end;

    

     Lm3: for V be RealUnitarySpace, W1,W2,W3 be Subspace of V st W1 is Subspace of W2 & W1 is Subspace of W3 holds W1 is Subspace of (W2 /\ W3)

    proof

      let V be RealUnitarySpace;

      let W1,W2,W3 be Subspace of V;

      assume

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

      now

        let v be VECTOR of V;

        assume v in W1;

        then v in W2 & v in W3 by A1, RUSUB_1: 1;

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

      end;

      hence thesis by RUSUB_1: 23;

    end;

    

     Lm4: for V be RealUnitarySpace, W1,W2,W3 be Subspace of V st W1 is Subspace of W2 holds W1 is Subspace of (W2 + W3)

    proof

      let V be RealUnitarySpace;

      let W1,W2,W3 be Subspace of V;

      

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

      assume W1 is Subspace of W2;

      hence thesis by A1, RUSUB_1: 21;

    end;

    

     Lm5: for V be RealUnitarySpace, W1,W2,W3 be Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds (W1 + W2) is Subspace of W3

    proof

      let V be RealUnitarySpace;

      let W1,W2,W3 be Subspace of V;

      assume

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

      now

        let v be VECTOR of V;

        assume v in (W1 + W2);

        then

        consider v1,v2 be VECTOR of V such that

         A2: v1 in W1 & v2 in W2 and

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

        v1 in W3 & v2 in W3 by A1, A2, RUSUB_1: 1;

        hence v in W3 by A3, RUSUB_1: 14;

      end;

      hence thesis by RUSUB_1: 23;

    end;

    theorem :: RUSUB_3:7

    

     Th7: for V be RealUnitarySpace, A,B be Subset of V st A c= B holds ( Lin A) is Subspace of ( Lin B)

    proof

      let V be RealUnitarySpace;

      let A,B be Subset of V;

      assume

       A1: A c= B;

      now

        let v be VECTOR of V;

        assume v in ( Lin A);

        then

        consider l be Linear_Combination of A such that

         A2: v = ( Sum l) by Th1;

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

        ( Sum l) = v by A2;

        hence v in ( Lin B) by Th1;

      end;

      hence thesis by RUSUB_1: 23;

    end;

    theorem :: RUSUB_3:8

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

    proof

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

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

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

      hence thesis by RUSUB_1: 20;

    end;

    theorem :: RUSUB_3:9

    for V be RealUnitarySpace, A,B be Subset of V holds ( Lin (A \/ B)) = (( Lin A) + ( Lin B))

    proof

      let V be RealUnitarySpace;

      let A,B be Subset of V;

      now

        deffunc G( object) = 0 ;

        let v be VECTOR of V;

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

        then

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

         A1: v = ( Sum l) by Th1;

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

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

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

        defpred C[ object] means $1 in C;

        defpred D[ object] means $1 in D;

        now

          let x be set;

          assume x in the carrier of V;

          then

          reconsider v = x as VECTOR of V;

          for f be Function of the carrier of V, REAL holds (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 ( C[x] implies F(x) in REAL ) & ( not C[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 ( C[x] implies (f . x) = F(x)) & ( not C[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 be VECTOR of V st not u in C holds (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 be VECTOR of V 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 be set;

          assume x in the carrier of V;

          then

          reconsider v = x as VECTOR of V;

          for g be Function of the carrier of V, REAL holds (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 be VECTOR of V 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 be VECTOR of V 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 be VECTOR of 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, RLVECT_3: 1;

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

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

      end;

      then

       A20: ( Lin (A \/ B)) is Subspace of (( Lin A) + ( Lin B)) by RUSUB_1: 23;

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

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

      hence thesis by A20, RUSUB_1: 20;

    end;

    theorem :: RUSUB_3:10

    for V be RealUnitarySpace, A,B be Subset of V holds ( Lin (A /\ B)) is Subspace of (( Lin A) /\ ( Lin B))

    proof

      let V be RealUnitarySpace;

      let A,B be Subset of V;

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

      hence thesis by Lm3;

    end;

    theorem :: RUSUB_3:11

    

     Th11: for V be RealUnitarySpace, A be Subset of V st A is linearly-independent holds ex B be Subset of V st A c= B & B is linearly-independent & ( Lin B) = the UNITSTR of V

    proof

      let V be RealUnitarySpace;

      let A be Subset of V;

      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 be set holds Z in Q iff Z in ( bool the carrier of V) & P[Z] from XFAMILY:sch 1;

       A2:

      now

        let Z be set;

        assume that

         A3: Z <> {} and

         A4: Z c= Q and

         A5: Z is c=-linear;

        set x = the Element of Z;

        x in Q by A3, A4;

        then

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

        set W = ( union Z);

        W c= the carrier of V

        proof

          let x be object;

          assume x in W;

          then

          consider X be set such that

           A7: x in X and

           A8: X in Z by TARSKI:def 4;

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

          hence thesis by A7;

        end;

        then

        reconsider W as Subset of V;

        

         A9: W is linearly-independent

        proof

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

          let l be Linear_Combination of W;

          assume that

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

           A11: ( Carrier l) <> {} ;

          consider f be Function such that

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

           A13: 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 A11, A12, RELAT_1: 42;

          set F = the Choice_Function of M;

          set S = ( rng F);

           A14:

          now

            assume {} in M;

            then

            consider x be object such that

             A15: x in ( dom f) and

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

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

            then

            consider X be set such that

             A17: x in X and

             A18: X in Z by A12, A15, TARSKI:def 4;

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

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

            hence contradiction by A12, A13, A15, A16;

          end;

          then

           A19: ( dom F) = M by RLVECT_3: 28;

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

          then

           A20: S is finite by FINSET_1: 8;

           A21:

          now

            let X be set;

            assume X in S;

            then

            consider x be object such that

             A22: x in ( dom F) and

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

            consider y be object such that

             A24: y in ( dom f) & (f . y) = x by A19, A22, FUNCT_1:def 3;

            

             A25: x = { C where C be Subset of V : y in C & C in Z } by A12, A13, A24;

            reconsider x as set by TARSKI: 1;

            X in x by A14, A19, A22, A23, ORDERS_1: 89;

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

            hence X in Z;

          end;

           A26:

          now

            let X,Y be set;

            assume X in S & Y in S;

            then X in Z & Y in Z by A21;

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

            hence X c= Y or Y c= X;

          end;

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

          then ( union S) in S by A26, A20, CARD_2: 62;

          then ( union S) in Z by A21;

          then

          consider B be Subset of V such that

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

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

          ( Carrier l) c= ( union S)

          proof

            let x be object;

            set X = (f . x);

            assume

             A29: x in ( Carrier l);

            then

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

            

             A31: (f . x) in M by A12, A29, FUNCT_1:def 3;

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

            then

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

            (F . X) in S by A19, A31, FUNCT_1:def 3;

            hence thesis by A32, TARSKI:def 4;

          end;

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

          hence thesis by A10, A11, A28;

        end;

        x c= W by A3, ZFMISC_1: 74;

        then A c= W by A6;

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

      end;

      

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

      assume A is linearly-independent;

      then Q <> {} by A1;

      then

      consider X be set such that

       A34: X in Q and

       A35: for Z be set 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 UNITSTR of V;

      then

      consider v be VECTOR of V such that

       A39: not (v in ( Lin B) iff v in the UNITSTR of V) by A33, RUSUB_1: 25;

      

       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( set) = zz;

            deffunc F( 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) = 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 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, RLVECT_3: 4;

            

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

            .= (( - (l . v)) * v) by A50, RLVECT_1: 4;

            then

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

            ((( - (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, RLVECT_1: 1, RUSUB_1: 15;

          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, Th2, 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 :: RUSUB_3:12

    

     Th12: for V be RealUnitarySpace, A be Subset of V st ( Lin A) = V holds ex B be Subset of V st B c= A & B is linearly-independent & ( Lin B) = V

    proof

      let V be RealUnitarySpace;

      let A be Subset of V;

      assume

       A1: ( Lin A) = V;

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

      consider Q be set such that

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

       A3:

      now

        let Z be set;

        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 be set 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 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) = 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 be set 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 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 RLVECT_3: 28;

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

          then

           A19: S is finite by FINSET_1: 8;

           A20:

          now

            let X be set;

            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 where C be Subset of V : 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 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 be set;

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

        W c= A

        proof

          let x be object;

          assume x in W;

          then

          consider X be set such that

           A32: x in X and

           A33: X in Z by TARSKI:def 4;

          ex B be Subset of V 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 RLVECT_3: 7;

      then Q <> {} by A2;

      then

      consider X be set such that

       A34: X in Q and

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

      consider B be Subset of V 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 be VECTOR of V st v in A holds v in ( Lin B);

        now

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

          let v be VECTOR of V;

          assume v in ( Lin A);

          then

          consider l be Linear_Combination of A such that

           A41: v = ( Sum l) by Th1;

          ( 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 Th1;

          hence v in ( Lin B) by Th5;

        end;

        then ( Lin A) is Subspace of ( Lin B) by RUSUB_1: 23;

        hence contradiction by A1, A39, RUSUB_1: 20;

      end;

      then

      consider v be VECTOR of 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( set) = ( In ( 0 , REAL ));

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

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

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

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

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

            now

              let u 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 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 be VECTOR of V 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 be Function of the carrier of V, REAL such that

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

             A54: 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 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 be VECTOR of V 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 be VECTOR of V;

              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, RLVECT_3: 4;

            

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

            .= (( - (l . v)) * v) by A55, RLVECT_1: 4;

            then

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

            ((( - (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, RUSUB_1: 15;

          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, Th2;

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

    end;

    begin

    definition

      let V be RealUnitarySpace;

      :: RUSUB_3:def2

      mode Basis of V -> Subset of V means

      : Def2: it is linearly-independent & ( Lin it ) = the UNITSTR of V;

      existence

      proof

        ( {} the carrier of V) is linearly-independent by RLVECT_3: 7;

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

        hence thesis;

      end;

    end

    theorem :: RUSUB_3:13

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

    proof

      let V be strict RealUnitarySpace, 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 Th11;

      reconsider B as Basis of V by A2, Def2;

      take B;

      thus thesis by A1;

    end;

    theorem :: RUSUB_3:14

    for V be RealUnitarySpace, A be Subset of V st ( Lin A) = V holds ex I be Basis of V st I c= A

    proof

      let V be RealUnitarySpace;

      let A be Subset of V;

      assume ( Lin A) = V;

      then

      consider B be Subset of V such that

       A1: B c= A and

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

      reconsider B as Basis of V by A2, Def2;

      take B;

      thus thesis by A1;

    end;

    theorem :: RUSUB_3:15

    

     Th15: for V be RealUnitarySpace, A be Subset of V st A is linearly-independent holds ex I be Basis of V st A c= I

    proof

      let V be RealUnitarySpace, 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) = the UNITSTR of V by Th11;

      reconsider B as Basis of V by A2, Def2;

      take B;

      thus thesis by A1;

    end;

    begin

    theorem :: RUSUB_3:16

    

     Th16: for V be RealUnitarySpace, L be Linear_Combination of V, A be Subset of V, F be FinSequence of V st ( rng F) c= the carrier of ( Lin A) holds ex K be Linear_Combination of A st ( Sum (L (#) F)) = ( Sum K)

    proof

      let V be RealUnitarySpace;

      let L be Linear_Combination of V;

      let A be Subset of V;

      defpred P[ Nat] means for F be FinSequence of V st ( rng F) c= the carrier of ( Lin A) & ( len F) = $1 holds ex K be Linear_Combination of A st ( Sum (L (#) F)) = ( Sum K);

      let F be FinSequence of V;

      assume

       A1: ( rng F) c= the carrier of ( Lin A);

      

       A2: ( len F) is Nat;

      

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

      proof

        let n be Nat;

        assume

         A4: P[n];

        let F be FinSequence of V such that

         A5: ( rng F) c= the carrier of ( Lin A) and

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

        consider G be FinSequence, x be object such that

         A7: F = (G ^ <*x*>) by A6, FINSEQ_2: 18;

        reconsider G, x9 = <*x*> as FinSequence of V by A7, FINSEQ_1: 36;

        

         A8: ( rng (G ^ <*x*>)) = (( rng G) \/ ( rng <*x*>)) by FINSEQ_1: 31

        .= (( rng G) \/ {x}) by FINSEQ_1: 38;

        then

         A9: ( rng G) c= ( rng F) by A7, XBOOLE_1: 7;

         {x} c= ( rng F) by A7, A8, XBOOLE_1: 7;

        then {x} c= the carrier of ( Lin A) by A5;

        then x in {x} implies x in the carrier of ( Lin A);

        then

         A10: x in ( Lin A) by STRUCT_0:def 5, TARSKI:def 1;

        then

         A11: x in V by RUSUB_1: 2;

        consider LA1 be Linear_Combination of A such that

         A12: x = ( Sum LA1) by A10, Th1;

        reconsider x as VECTOR of V by A11, STRUCT_0:def 5;

        ( len (G ^ <*x*>)) = (( len G) + ( len <*x*>)) by FINSEQ_1: 22

        .= (( len G) + 1) by FINSEQ_1: 39;

        then

        consider LA2 be Linear_Combination of A such that

         A13: ( Sum (L (#) G)) = ( Sum LA2) by A4, A5, A6, A7, A9, XBOOLE_1: 1;

        ((L . x) * LA1) is Linear_Combination of A by RLVECT_2: 44;

        then

         A14: (LA2 + ((L . x) * LA1)) is Linear_Combination of A by RLVECT_2: 38;

        ( Sum (L (#) F)) = ( Sum ((L (#) G) ^ (L (#) x9))) by A7, RLVECT_3: 34

        .= (( Sum LA2) + ( Sum (L (#) x9))) by A13, RLVECT_1: 41

        .= (( Sum LA2) + ( Sum <*((L . x) * x)*>)) by RLVECT_2: 26

        .= (( Sum LA2) + ((L . x) * ( Sum LA1))) by A12, RLVECT_1: 44

        .= (( Sum LA2) + ( Sum ((L . x) * LA1))) by RLVECT_3: 2

        .= ( Sum (LA2 + ((L . x) * LA1))) by RLVECT_3: 1;

        hence thesis by A14;

      end;

      

       A15: P[ 0 ]

      proof

        let F be FinSequence of V;

        assume that ( rng F) c= the carrier of ( Lin A) and

         A16: ( len F) = 0 ;

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

        then (L (#) F) = ( <*> the carrier of V) by RLVECT_2: 25;

        

        then

         A17: ( Sum (L (#) F)) = ( 0. V) by RLVECT_1: 43

        .= ( Sum ( ZeroLC V)) by RLVECT_2: 30;

        ( ZeroLC V) is Linear_Combination of A by RLVECT_2: 22;

        hence thesis by A17;

      end;

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

      hence thesis by A1, A2;

    end;

    theorem :: RUSUB_3:17

    for V be RealUnitarySpace, L be Linear_Combination of V, A be Subset of V st ( Carrier L) c= the carrier of ( Lin A) holds ex K be Linear_Combination of A st ( Sum L) = ( Sum K)

    proof

      let V be RealUnitarySpace;

      let L be Linear_Combination of V, A be Subset of V;

      consider F be FinSequence of V such that F is one-to-one and

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

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

      assume ( Carrier L) c= the carrier of ( Lin A);

      then

      consider K be Linear_Combination of A such that

       A3: ( Sum (L (#) F)) = ( Sum K) by A1, Th16;

      take K;

      thus thesis by A2, A3;

    end;

    theorem :: RUSUB_3:18

    

     Th18: for V be RealUnitarySpace, W be Subspace of V, L be Linear_Combination of V st ( Carrier L) c= the carrier of W holds for K be Linear_Combination of W st K = (L | the carrier of W) holds ( Carrier L) = ( Carrier K) & ( Sum L) = ( Sum K)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let L be Linear_Combination of V such that

       A1: ( Carrier L) c= the carrier of W;

      let K be Linear_Combination of W such that

       A2: K = (L | the carrier of W);

      

       A3: ( dom K) = the carrier of W by FUNCT_2:def 1;

      now

        let x be object;

        assume x in ( Carrier K);

        then

        consider w be VECTOR of W such that

         A4: x = w and

         A5: (K . w) <> 0 ;

        

         A6: w is VECTOR of V by RUSUB_1: 3;

        (L . w) <> 0 by A2, A3, A5, FUNCT_1: 47;

        hence x in ( Carrier L) by A4, A6;

      end;

      then

       A7: ( Carrier K) c= ( Carrier L);

      consider G be FinSequence of W such that

       A8: G is one-to-one & ( rng G) = ( Carrier K) and

       A9: ( Sum K) = ( Sum (K (#) G)) by RLVECT_2:def 8;

      consider F be FinSequence of V such that

       A10: F is one-to-one and

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

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

      now

        let x be object;

        assume

         A13: x in ( Carrier L);

        then

        consider v be VECTOR of V such that

         A14: x = v and

         A15: (L . v) <> 0 ;

        (K . v) <> 0 by A1, A2, A3, A13, A14, A15, FUNCT_1: 47;

        hence x in ( Carrier K) by A1, A13, A14;

      end;

      then

       A16: ( Carrier L) c= ( Carrier K);

      then

       A17: ( Carrier K) = ( Carrier L) by A7;

      then (F,G) are_fiberwise_equipotent by A10, A11, A8, RFINSEQ: 26;

      then

      consider P be Permutation of ( dom G) such that

       A18: F = (G * P) by RFINSEQ: 4;

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

      then

       A19: ( dom (K (#) G)) = ( dom G) by FINSEQ_3: 29;

      then

      reconsider q = ((K (#) G) * P) as FinSequence of W by FINSEQ_2: 47;

      

       A20: ( len q) = ( len (K (#) G)) by A19, FINSEQ_2: 44;

      then ( len q) = ( len G) by RLVECT_2:def 7;

      then

       A21: ( dom q) = ( dom G) by FINSEQ_3: 29;

      set p = (L (#) F);

      

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

      ( rng q) c= the carrier of W by FINSEQ_1:def 4;

      then ( rng q) c= the carrier of V by A22;

      then

      reconsider q9 = q as FinSequence of V by FINSEQ_1:def 4;

      consider f be sequence of the carrier of W such that

       A23: ( Sum q) = (f . ( len q)) and

       A24: (f . 0 ) = ( 0. W) and

       A25: for i be Nat, w be VECTOR of W st i < ( len q) & w = (q . (i + 1)) holds (f . (i + 1)) = ((f . i) + w) by RLVECT_1:def 12;

      ( dom f) = NAT & ( rng f) c= the carrier of W by FUNCT_2:def 1, RELAT_1:def 19;

      then

      reconsider f9 = f as sequence of the carrier of V by A22, FUNCT_2: 2, XBOOLE_1: 1;

      

       A26: for i be Nat, v be VECTOR of V st i < ( len q9) & v = (q9 . (i + 1)) holds (f9 . (i + 1)) = ((f9 . i) + v)

      proof

        let i be Nat, v be VECTOR of V;

        assume that

         A27: i < ( len q9) and

         A28: v = (q9 . (i + 1));

        1 <= (i + 1) & (i + 1) <= ( len q) by A27, NAT_1: 11, NAT_1: 13;

        then (i + 1) in ( dom q) by FINSEQ_3: 25;

        then

        reconsider v9 = v as VECTOR of W by A28, FINSEQ_2: 11;

        (f . (i + 1)) = ((f . i) + v9) by A25, A27, A28;

        hence thesis by RUSUB_1: 6;

      end;

      

       A29: ( len G) = ( len F) by A18, FINSEQ_2: 44;

      then

       A30: ( dom G) = ( dom F) by FINSEQ_3: 29;

      ( len G) = ( len (L (#) F)) by A29, RLVECT_2:def 7;

      then

       A31: ( dom p) = ( dom G) by FINSEQ_3: 29;

      

       A32: ( dom q) = ( dom (K (#) G)) by A20, FINSEQ_3: 29;

      now

        let i be Nat;

        set v = (F /. i);

        set j = (P . i);

        assume

         A33: i in ( dom p);

        then

         A34: (F /. i) = (F . i) by A31, A30, PARTFUN1:def 6;

        then v in ( rng F) by A31, A30, A33, FUNCT_1:def 3;

        then

        reconsider w = v as VECTOR of W by A17, A11;

        ( dom P) = ( dom G) & ( rng P) = ( dom G) by FUNCT_2: 52, FUNCT_2:def 3;

        then

         A35: j in ( dom G) by A31, A33, FUNCT_1:def 3;

        then j in ( Seg ( card G)) by FINSEQ_1:def 3;

        then

        reconsider j as Element of NAT ;

        

         A36: (G /. j) = (G . (P . i)) by A35, PARTFUN1:def 6

        .= v by A18, A31, A30, A33, A34, FUNCT_1: 12;

        (q . i) = ((K (#) G) . j) by A31, A21, A33, FUNCT_1: 12

        .= ((K . w) * w) by A32, A21, A35, A36, RLVECT_2:def 7

        .= ((L . v) * w) by A2, A3, FUNCT_1: 47

        .= ((L . v) * v) by RUSUB_1: 7;

        hence (p . i) = (q . i) by A33, RLVECT_2:def 7;

      end;

      then

       A37: (L (#) F) = ((K (#) G) * P) by A31, A21, FINSEQ_1: 13;

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

      then ( dom G) = ( dom (K (#) G)) by FINSEQ_3: 29;

      then

      reconsider P as Permutation of ( dom (K (#) G));

      q = ((K (#) G) * P);

      then

       A38: ( Sum (K (#) G)) = ( Sum q) by RLVECT_2: 7;

      

       A39: (f9 . ( len q9)) is Element of V;

      (f9 . 0 ) = ( 0. V) by A24, RUSUB_1: 4;

      hence thesis by A7, A16, A12, A9, A37, A38, A23, A26, A39, RLVECT_1:def 12;

    end;

    theorem :: RUSUB_3:19

    

     Th19: for V be RealUnitarySpace, W be Subspace of V, K be Linear_Combination of W holds ex L be Linear_Combination of V st ( Carrier K) = ( Carrier L) & ( Sum K) = ( Sum L)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let K be Linear_Combination of W;

      defpred P[ object, object] means ($1 in W & $2 = (K . $1)) or ( not $1 in W & $2 = 0 );

      reconsider K9 = K as Function of the carrier of W, REAL ;

      

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

      then

      reconsider C = ( Carrier K) as finite Subset of V by XBOOLE_1: 1;

      

       A2: for x be object st x in the carrier of V holds ex y be object st y in REAL & P[x, y]

      proof

        let x be object;

        assume x in the carrier of V;

        then

        reconsider x as VECTOR of V;

        per cases ;

          suppose

           A3: x in W;

          then

          reconsider x as VECTOR of W by STRUCT_0:def 5;

           P[x, (K . x)] by A3;

          hence thesis;

        end;

          suppose

           A4: not x in W;

           0 in REAL by XREAL_0:def 1;

          hence thesis by A4;

        end;

      end;

      ex L be Function of the carrier of V, REAL st for x be object st x in the carrier of V holds P[x, (L . x)] from FUNCT_2:sch 1( A2);

      then

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

       A5: for x be object st x in the carrier of V holds P[x, (L . x)];

       A6:

      now

        let v be VECTOR of V;

        assume not v in C;

        then P[v, (K . v)] & not v in C & v in the carrier of W or P[v, 0 ] by STRUCT_0:def 5;

        then P[v, (K . v)] & (K . v) = 0 or P[v, 0 ];

        hence (L . v) = 0 by A5;

      end;

      L is Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

      then

      reconsider L as Linear_Combination of V by A6, RLVECT_2:def 3;

      reconsider L9 = (L | the carrier of W) as Function of the carrier of W, REAL by A1, FUNCT_2: 32;

      take L;

      now

        let x be object;

        assume x in ( Carrier L) & not x in the carrier of W;

        then (ex v be VECTOR of V st x = v & (L . v) <> 0 ) & not x in W by STRUCT_0:def 5;

        hence contradiction by A5;

      end;

      then

       A7: ( Carrier L) c= the carrier of W;

      now

        let x be object;

        assume

         A8: x in the carrier of W;

        then P[x, (L . x)] by A5, A1;

        hence (K9 . x) = (L9 . x) by A8, FUNCT_1: 49, STRUCT_0:def 5;

      end;

      then K9 = L9 by FUNCT_2: 12;

      hence thesis by A7, Th18;

    end;

    theorem :: RUSUB_3:20

    

     Th20: for V be RealUnitarySpace, W be Subspace of V, L be Linear_Combination of V st ( Carrier L) c= the carrier of W holds ex K be Linear_Combination of W st ( Carrier K) = ( Carrier L) & ( Sum K) = ( Sum L)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let L be Linear_Combination of V;

      assume

       A1: ( Carrier L) c= the carrier of W;

      then

      reconsider C = ( Carrier L) as finite Subset of W;

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

      then

      reconsider K = (L | the carrier of W) as Function of the carrier of W, REAL by FUNCT_2: 32;

      

       A2: K is Element of ( Funcs (the carrier of W, REAL )) by FUNCT_2: 8;

      

       A3: ( dom K) = the carrier of W by FUNCT_2:def 1;

      now

        let w be VECTOR of W;

        

         A4: w is VECTOR of V by RUSUB_1: 3;

        assume not w in C;

        then (L . w) = 0 by A4;

        hence (K . w) = 0 by A3, FUNCT_1: 47;

      end;

      then

      reconsider K as Linear_Combination of W by A2, RLVECT_2:def 3;

      take K;

      thus thesis by A1, Th18;

    end;

    theorem :: RUSUB_3:21

    

     Th21: for V be RealUnitarySpace, I be Basis of V, v be VECTOR of V holds v in ( Lin I)

    proof

      let V be RealUnitarySpace;

      let I be Basis of V;

      let v be VECTOR of V;

      v in the UNITSTR of V by STRUCT_0:def 5;

      hence thesis by Def2;

    end;

    theorem :: RUSUB_3:22

    

     Th22: for V be RealUnitarySpace, W be Subspace of V, A be Subset of W st A is linearly-independent holds A is linearly-independent Subset of V

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let A be Subset of W;

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

      then

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

      assume

       A1: A is linearly-independent;

      now

        assume A9 is linearly-dependent;

        then

        consider L be Linear_Combination of A9 such that

         A2: ( Sum L) = ( 0. V) and

         A3: ( Carrier L) <> {} ;

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

        then

        consider LW be Linear_Combination of W such that

         A4: ( Carrier LW) = ( Carrier L) and

         A5: ( Sum LW) = ( Sum L) by Th20, XBOOLE_1: 1;

        reconsider LW as Linear_Combination of A by A4, RLVECT_2:def 6;

        ( Sum LW) = ( 0. W) by A2, A5, RUSUB_1: 4;

        hence contradiction by A1, A3, A4;

      end;

      hence thesis;

    end;

    theorem :: RUSUB_3:23

    for V be RealUnitarySpace, W be Subspace of V, A be Subset of V st A is linearly-independent & A c= the carrier of W holds A is linearly-independent Subset of W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let A be Subset of V such that

       A1: A is linearly-independent and

       A2: A c= the carrier of W;

      reconsider A9 = A as Subset of W by A2;

      now

        assume A9 is linearly-dependent;

        then

        consider K be Linear_Combination of A9 such that

         A3: ( Sum K) = ( 0. W) and

         A4: ( Carrier K) <> {} ;

        consider L be Linear_Combination of V such that

         A5: ( Carrier L) = ( Carrier K) and

         A6: ( Sum L) = ( Sum K) by Th19;

        reconsider L as Linear_Combination of A by A5, RLVECT_2:def 6;

        ( Sum L) = ( 0. V) by A3, A6, RUSUB_1: 4;

        hence contradiction by A1, A4, A5;

      end;

      hence thesis;

    end;

    theorem :: RUSUB_3:24

    for V be RealUnitarySpace, W be Subspace of V, A be Basis of W holds ex B be Basis of V st A c= B

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let A be Basis of W;

      A is linearly-independent by Def2;

      then

      reconsider B = A as linearly-independent Subset of V by Th22;

      consider I be Basis of V such that

       A1: B c= I by Th15;

      take I;

      thus thesis by A1;

    end;

    theorem :: RUSUB_3:25

    

     Th25: for V be RealUnitarySpace, A be Subset of V st A is linearly-independent holds for v be VECTOR of V st v in A holds for B be Subset of V st B = (A \ {v}) holds not v in ( Lin B)

    proof

      let V be RealUnitarySpace;

      let A be Subset of V such that

       A1: A is linearly-independent;

      let v be VECTOR of V;

      assume v in A;

      then

       A2: {v} is Subset of A by SUBSET_1: 41;

      let B be Subset of V such that

       A3: B = (A \ {v});

      B c= A by A3, XBOOLE_1: 36;

      then

       A4: (B \/ {v}) c= (A \/ A) by A2, XBOOLE_1: 13;

      assume v in ( Lin B);

      then

      consider L be Linear_Combination of B such that

       A5: v = ( Sum L) by Th1;

       {v} is linearly-independent by A1, A2, RLVECT_3: 5;

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

      then ( Carrier L) is non empty by A5, RLVECT_2: 34;

      then

       A6: ex w be object st w in ( Carrier L);

      v in {v} by TARSKI:def 1;

      then v in ( Lin {v}) by Th2;

      then

      consider K be Linear_Combination of {v} such that

       A7: v = ( Sum K) by Th1;

      

       A8: ( Carrier L) c= B & ( Carrier K) c= {v} by RLVECT_2:def 6;

      then (( Carrier L) \/ ( Carrier K)) c= (B \/ {v}) by XBOOLE_1: 13;

      then ( Carrier (L - K)) c= (( Carrier L) \/ ( Carrier K)) & (( Carrier L) \/ ( Carrier K)) c= A by A4, RLVECT_2: 55;

      then ( Carrier (L - K)) c= A;

      then

       A9: (L - K) is Linear_Combination of A by RLVECT_2:def 6;

      

       A10: for x be VECTOR of V holds x in ( Carrier L) implies (K . x) = 0

      proof

        let x be VECTOR of V;

        assume x in ( Carrier L);

        then not x in ( Carrier K) by A3, A8, XBOOLE_0:def 5;

        hence thesis;

      end;

      now

        let x be object such that

         A11: x in ( Carrier L) and

         A12: not x in ( Carrier (L - K));

        reconsider x as VECTOR of V by A11;

        

         A13: (L . x) <> 0 by A11, RLVECT_2: 19;

        ((L - K) . x) = ((L . x) - (K . x)) by RLVECT_2: 54

        .= ((L . x) - 0 ) by A10, A11

        .= (L . x);

        hence contradiction by A12, A13;

      end;

      then

       A14: ( Carrier L) c= ( Carrier (L - K));

      ( 0. V) = (( Sum L) + ( - ( Sum K))) by A5, A7, RLVECT_1: 5

      .= (( Sum L) + ( Sum ( - K))) by RLVECT_3: 3

      .= ( Sum (L - K)) by RLVECT_3: 1;

      hence contradiction by A1, A6, A9, A14;

    end;

    

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

    proof

      let X be set, x be set such that

       A1: not x in X;

      now

        assume X meets {x};

        then

        consider y be object such that

         A2: y in (X /\ {x}) by XBOOLE_0: 4;

        y in X & y in {x} by A2, XBOOLE_0:def 4;

        hence contradiction by A1, TARSKI:def 1;

      end;

      hence thesis by XBOOLE_1: 83;

    end;

    theorem :: RUSUB_3:26

    for V be RealUnitarySpace, I be Basis of V, A be non empty Subset of V st A misses I holds for B be Subset of V st B = (I \/ A) holds B is linearly-dependent

    proof

      let V be RealUnitarySpace;

      let I be Basis of V;

      let A be non empty Subset of V such that

       A1: A misses I;

      consider v be object such that

       A2: v in A by XBOOLE_0:def 1;

      let B be Subset of V such that

       A3: B = (I \/ A);

      

       A4: A c= B by A3, XBOOLE_1: 7;

      reconsider v as VECTOR of V by A2;

      reconsider Bv = (B \ {v}) as Subset of V;

      

       A5: (I \ {v}) c= (B \ {v}) by A3, XBOOLE_1: 7, XBOOLE_1: 33;

       not v in I by A1, A2, XBOOLE_0: 3;

      then I c= Bv by A5, Lm6;

      then

       A6: ( Lin I) is Subspace of ( Lin Bv) by Th7;

      assume

       A7: B is linearly-independent;

      v in ( Lin I) by Th21;

      hence contradiction by A7, A2, A4, A6, Th25, RUSUB_1: 1;

    end;

    theorem :: RUSUB_3:27

    for V be RealUnitarySpace, W be Subspace of V, A be Subset of V st A c= the carrier of W holds ( Lin A) is Subspace of W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let A be Subset of V;

      assume

       A1: A c= the carrier of W;

      now

        let w be object;

        assume w in the carrier of ( Lin A);

        then w in ( Lin A) by STRUCT_0:def 5;

        then

        consider L be Linear_Combination of A such that

         A2: w = ( Sum L) by Th1;

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

        then ex K be Linear_Combination of W st ( Carrier K) = ( Carrier L) & ( Sum L) = ( Sum K) by A1, Th20, XBOOLE_1: 1;

        hence w in the carrier of W by A2;

      end;

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

      hence thesis by RUSUB_1: 22;

    end;

    theorem :: RUSUB_3:28

    for V be RealUnitarySpace, W be Subspace of V, A be Subset of V, B be Subset of W st A = B holds ( Lin A) = ( Lin B)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let A be Subset of V, B be Subset of W;

      reconsider B9 = ( Lin B), V9 = V as RealUnitarySpace;

      

       A1: B9 is Subspace of V9 by RUSUB_1: 21;

      assume

       A2: A = B;

      now

        let x be object;

        assume x in the carrier of ( Lin A);

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

        then

        consider L be Linear_Combination of A such that

         A3: x = ( Sum L) by Th1;

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

        then

        consider K be Linear_Combination of W such that

         A4: ( Carrier K) = ( Carrier L) and

         A5: ( Sum K) = ( Sum L) by A2, Th20, XBOOLE_1: 1;

        reconsider K as Linear_Combination of B by A2, A4, RLVECT_2:def 6;

        x = ( Sum K) by A3, A5;

        then x in ( Lin B) by Th1;

        hence x in the carrier of ( Lin B) by STRUCT_0:def 5;

      end;

      then

       A6: the carrier of ( Lin A) c= the carrier of ( Lin B);

      now

        let x be object;

        assume x in the carrier of ( Lin B);

        then x in ( Lin B) by STRUCT_0:def 5;

        then

        consider K be Linear_Combination of B such that

         A7: x = ( Sum K) by Th1;

        consider L be Linear_Combination of V such that

         A8: ( Carrier L) = ( Carrier K) and

         A9: ( Sum L) = ( Sum K) by Th19;

        reconsider L as Linear_Combination of A by A2, A8, RLVECT_2:def 6;

        x = ( Sum L) by A7, A9;

        then x in ( Lin A) by Th1;

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

      end;

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

      then the carrier of ( Lin A) = the carrier of ( Lin B) by A6;

      hence thesis by A1, RUSUB_1: 24;

    end;

    begin

    theorem :: RUSUB_3:29

    

     Th29: for V be RealUnitarySpace, v be VECTOR of V, x be set holds x in ( Lin {v}) iff ex a be Real st x = (a * v)

    proof

      deffunc F( set) = ( In ( 0 , REAL ));

      let V be RealUnitarySpace;

      let v be VECTOR of V;

      let x be set;

      thus x in ( Lin {v}) implies ex a be Real st x = (a * v)

      proof

        assume x in ( Lin {v});

        then

        consider l be Linear_Combination of {v} such that

         A1: x = ( Sum l) by Th1;

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

        hence thesis by A1;

      end;

      given a be Real such that

       A2: x = (a * v);

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

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

       A3: (f . v) = a and

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

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

      now

        let z be VECTOR of V;

        assume not z in {v};

        then z <> v by TARSKI:def 1;

        hence (f . z) = 0 by A4;

      end;

      then

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

      ( Carrier f) c= {v}

      proof

        let x be object;

        assume

         A5: x in ( Carrier f);

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

        then x = v by A4, A5;

        hence thesis by TARSKI:def 1;

      end;

      then

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

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

      hence thesis by Th1;

    end;

    theorem :: RUSUB_3:30

    for V be RealUnitarySpace, v be VECTOR of V holds v in ( Lin {v})

    proof

      let V be RealUnitarySpace;

      let v be VECTOR of V;

      v in {v} by TARSKI:def 1;

      hence thesis by Th2;

    end;

    theorem :: RUSUB_3:31

    for V be RealUnitarySpace, v,w be VECTOR of V, x be set holds x in (v + ( Lin {w})) iff ex a be Real st x = (v + (a * w))

    proof

      let V be RealUnitarySpace;

      let v,w be VECTOR of V;

      let x be set;

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

      proof

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

        then

        consider u be VECTOR of V such that

         A1: u in ( Lin {w}) and

         A2: x = (v + u) by RUSUB_2: 63;

        ex a be Real st u = (a * w) by A1, Th29;

        hence thesis by A2;

      end;

      given a be Real such that

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

      (a * w) in ( Lin {w}) by Th29;

      hence thesis by A3, RUSUB_2: 63;

    end;

    theorem :: RUSUB_3:32

    

     Th32: for V be RealUnitarySpace, w1,w2 be VECTOR of V, x be set holds x in ( Lin {w1, w2}) iff ex a,b be Real st x = ((a * w1) + (b * w2))

    proof

      let V be RealUnitarySpace;

      let w1,w2 be VECTOR of V;

      let x be set;

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

      proof

        assume

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

        now

          per cases ;

            suppose w1 = w2;

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

            then

            consider a be Real such that

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

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

            .= ((a * w1) + ( 0 * w2)) by RLVECT_1: 10;

            hence thesis;

          end;

            suppose

             A3: w1 <> w2;

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

             A4: x = ( Sum l) by A1, Th1;

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

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      given a,b be Real such that

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

      now

        per cases ;

          suppose

           A6: w1 = w2;

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

          then x in ( Lin {w1}) by Th29;

          hence thesis by A6, ENUMSET1: 29;

        end;

          suppose

           A7: w1 <> w2;

          deffunc F( set) = ( In ( 0 , REAL ));

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

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

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

           A9: for u be VECTOR of V st u <> w1 & u <> w2 holds (f . u) = F(u) from FUNCT_2:sch 7( A7);

          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 {w1, w2};

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

            hence (f . u) = 0 by A9;

          end;

          then

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

          ( Carrier f) c= {w1, w2}

          proof

            let x be object;

            assume that

             A10: x in ( Carrier f) and

             A11: not x in {w1, w2};

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

            then (f . x) = 0 by A9, A10;

            hence contradiction by A10, RLVECT_2: 19;

          end;

          then

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

          x = ( Sum f) by A5, A7, A8, RLVECT_2: 33;

          hence thesis by Th1;

        end;

      end;

      hence thesis;

    end;

    theorem :: RUSUB_3:33

    for V be RealUnitarySpace, w1,w2 be VECTOR of V holds w1 in ( Lin {w1, w2}) & w2 in ( Lin {w1, w2})

    proof

      let V be RealUnitarySpace;

      let w1,w2 be VECTOR of V;

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

      hence thesis by Th2;

    end;

    theorem :: RUSUB_3:34

    for V be RealUnitarySpace, v,w1,w2 be VECTOR of V, x be set holds x in (v + ( Lin {w1, w2})) iff ex a,b be Real st x = ((v + (a * w1)) + (b * w2))

    proof

      let V be RealUnitarySpace;

      let v,w1,w2 be VECTOR of V;

      let x be set;

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

      proof

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

        then

        consider u be VECTOR of V such that

         A1: u in ( Lin {w1, w2}) and

         A2: x = (v + u) by RUSUB_2: 63;

        consider a,b be Real such that

         A3: u = ((a * w1) + (b * w2)) by A1, Th32;

        take a, b;

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

      end;

      given a,b be Real such that

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

      ((a * w1) + (b * w2)) in ( Lin {w1, w2}) by Th32;

      then (v + ((a * w1) + (b * w2))) in (v + ( Lin {w1, w2})) by RUSUB_2: 63;

      hence thesis by A4, RLVECT_1:def 3;

    end;

    theorem :: RUSUB_3:35

    

     Th35: for V be RealUnitarySpace, v1,v2,v3 be VECTOR of V, x be set holds x in ( Lin {v1, v2, v3}) iff ex a,b,c be Real st x = (((a * v1) + (b * v2)) + (c * v3))

    proof

      let V be RealUnitarySpace;

      let v1,v2,v3 be VECTOR of V;

      let x be set;

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

      proof

        assume

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

        now

          per cases ;

            suppose

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

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

             A3: x = ( Sum l) by A1, Th1;

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

            hence thesis;

          end;

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

            then

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

            now

              per cases by A4, ENUMSET1: 30;

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

                then

                consider a,b be Real such that

                 A5: x = ((a * v1) + (b * v2)) by A1, Th32;

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

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

                hence thesis;

              end;

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

                then

                consider a,b be Real such that

                 A6: x = ((a * v1) + (b * v3)) by A1, Th32;

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

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

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      given a,b,c be Real such that

       A7: x = (((a * v1) + (b * v2)) + (c * v3));

      now

        per cases ;

          suppose

           A8: v1 = v2 or v1 = v3 or v2 = v3;

          now

            per cases by A8;

              suppose v1 = v2;

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

              hence thesis by Th32;

            end;

              suppose

               A9: v1 = v3;

              

              then

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

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

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

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

              hence thesis by A10, Th32;

            end;

              suppose

               A11: v2 = v3;

              

              then

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

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

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

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

              hence thesis by A12, Th32;

            end;

          end;

          hence thesis;

        end;

          suppose

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

          deffunc F( set) = ( In ( 0 , REAL ));

          

           A14: v1 <> v3 by A13;

          

           A15: v2 <> v3 by A13;

          

           A16: v1 <> v2 by A13;

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

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

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

           A18: for v be VECTOR of V st v <> v1 & v <> v2 & v <> v3 holds (f . v) = F(v) from RLVECT_4:sch 1( A16, A14, A15);

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

          now

            let v be VECTOR of V;

            assume

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

            then

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

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

            hence (f . v) = 0 by A18, A20;

          end;

          then

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

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

          proof

            let x be object;

            assume that

             A21: x in ( Carrier f) and

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

            

             A23: x <> v3 by A22, ENUMSET1:def 1;

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

            then (f . x) = 0 by A18, A21, A23;

            hence thesis by A21, RLVECT_2: 19;

          end;

          then

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

          x = ( Sum f) by A7, A13, A17, RLVECT_4: 6;

          hence thesis by Th1;

        end;

      end;

      hence thesis;

    end;

    theorem :: RUSUB_3:36

    for V be RealUnitarySpace, w1,w2,w3 be VECTOR of V holds w1 in ( Lin {w1, w2, w3}) & w2 in ( Lin {w1, w2, w3}) & w3 in ( Lin {w1, w2, w3})

    proof

      let V be RealUnitarySpace;

      let w1,w2,w3 be VECTOR of V;

      

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

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

      hence thesis by A1, Th2;

    end;

    theorem :: RUSUB_3:37

    for V be RealUnitarySpace, v,w1,w2,w3 be VECTOR of V, x be set holds x in (v + ( Lin {w1, w2, w3})) iff ex a,b,c be Real st x = (((v + (a * w1)) + (b * w2)) + (c * w3))

    proof

      let V be RealUnitarySpace;

      let v,w1,w2,w3 be VECTOR of V;

      let x be set;

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

      proof

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

        then

        consider u be VECTOR of V such that

         A1: u in ( Lin {w1, w2, w3}) and

         A2: x = (v + u) by RUSUB_2: 63;

        consider a,b,c be Real such that

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

        take a, b, c;

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

        hence thesis by RLVECT_1:def 3;

      end;

      given a,b,c be Real such that

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

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

      then (v + (((a * w1) + (b * w2)) + (c * w3))) in (v + ( Lin {w1, w2, w3})) by RUSUB_2: 63;

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

      hence thesis by A4, RLVECT_1:def 3;

    end;

    theorem :: RUSUB_3:38

    for V be RealUnitarySpace, v,w be VECTOR of V st v in ( Lin {w}) & v <> ( 0. V) holds ( Lin {v}) = ( Lin {w})

    proof

      let V be RealUnitarySpace;

      let v,w be VECTOR of V;

      assume that

       A1: v in ( Lin {w}) and

       A2: v <> ( 0. V);

      consider a be Real such that

       A3: v = (a * w) by A1, Th29;

      now

        let u be VECTOR of V;

        

         A4: a <> 0 by A2, A3, RLVECT_1: 10;

        thus u in ( Lin {v}) implies u in ( Lin {w})

        proof

          assume u in ( Lin {v});

          then

          consider b be Real such that

           A5: u = (b * v) by Th29;

          u = ((b * a) * w) by A3, A5, RLVECT_1:def 7;

          hence thesis by Th29;

        end;

        assume u in ( Lin {w});

        then

        consider b be Real such that

         A6: u = (b * w) by Th29;

        ((a " ) * v) = (((a " ) * a) * w) by A3, RLVECT_1:def 7

        .= (1 * w) by A4, XCMPLX_0:def 7

        .= w by RLVECT_1:def 8;

        then u = ((b * (a " )) * v) by A6, RLVECT_1:def 7;

        hence u in ( Lin {v}) by Th29;

      end;

      hence thesis by RUSUB_1: 25;

    end;

    theorem :: RUSUB_3:39

    for V be RealUnitarySpace, v1,v2,w1,w2 be VECTOR of V st v1 <> v2 & {v1, v2} is linearly-independent & v1 in ( Lin {w1, w2}) & v2 in ( Lin {w1, w2}) holds ( Lin {w1, w2}) = ( Lin {v1, v2}) & {w1, w2} is linearly-independent & w1 <> w2

    proof

      let V be RealUnitarySpace;

      let v1,v2,w1,w2 be VECTOR of V;

      assume that

       A1: v1 <> v2 and

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

       A3: v1 in ( Lin {w1, w2}) and

       A4: v2 in ( Lin {w1, w2});

      consider r1,r2 be Real such that

       A5: v1 = ((r1 * w1) + (r2 * w2)) by A3, Th32;

      consider r3,r4 be Real such that

       A6: v2 = ((r3 * w1) + (r4 * w2)) by A4, Th32;

      set t = ((r1 * r4) - (r2 * r3));

       A7:

      now

        assume r1 = 0 & r2 = 0 ;

        

        then v1 = (( 0. V) + ( 0 * w2)) by A5, RLVECT_1: 10

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

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

        hence contradiction by A2, RLVECT_3: 11;

      end;

      now

        assume

         A8: (r1 * r4) = (r2 * r3);

        now

          per cases by A7;

            suppose

             A9: r1 <> 0 ;

            (((r1 " ) * r1) * r4) = ((r1 " ) * (r2 * r3)) by A8, XCMPLX_1: 4;

            then (1 * r4) = ((r1 " ) * (r2 * r3)) by A9, XCMPLX_0:def 7;

            

            then v2 = ((r3 * w1) + ((r3 * ((r1 " ) * r2)) * w2)) by A6

            .= ((r3 * w1) + (r3 * (((r1 " ) * r2) * w2))) by RLVECT_1:def 7

            .= ((r3 * 1) * (w1 + (((r1 " ) * r2) * w2))) by RLVECT_1:def 5

            .= ((r3 * ((r1 " ) * r1)) * (w1 + (((r1 " ) * r2) * w2))) by A9, XCMPLX_0:def 7

            .= (((r3 * (r1 " )) * r1) * (w1 + (((r1 " ) * r2) * w2)))

            .= ((r3 * (r1 " )) * (r1 * (w1 + (((r1 " ) * r2) * w2)))) by RLVECT_1:def 7

            .= ((r3 * (r1 " )) * ((r1 * w1) + (r1 * (((r1 " ) * r2) * w2)))) by RLVECT_1:def 5

            .= ((r3 * (r1 " )) * ((r1 * w1) + ((r1 * ((r1 " ) * r2)) * w2))) by RLVECT_1:def 7

            .= ((r3 * (r1 " )) * ((r1 * w1) + (((r1 * (r1 " )) * r2) * w2)))

            .= ((r3 * (r1 " )) * ((r1 * w1) + ((1 * r2) * w2))) by A9, XCMPLX_0:def 7

            .= ((r3 * (r1 " )) * ((r1 * w1) + (r2 * w2)));

            hence contradiction by A1, A2, A5, RLVECT_3: 12;

          end;

            suppose

             A10: r2 <> 0 ;

            ((r2 " ) * (r1 * r4)) = ((r2 " ) * (r2 * r3)) by A8

            .= (((r2 " ) * r2) * r3)

            .= (1 * r3) by A10, XCMPLX_0:def 7

            .= r3;

            

            then v2 = (((r4 * ((r2 " ) * r1)) * w1) + (r4 * w2)) by A6

            .= ((r4 * (((r2 " ) * r1) * w1)) + (r4 * w2)) by RLVECT_1:def 7

            .= ((r4 * 1) * ((((r2 " ) * r1) * w1) + w2)) by RLVECT_1:def 5

            .= ((r4 * ((r2 " ) * r2)) * ((((r2 " ) * r1) * w1) + w2)) by A10, XCMPLX_0:def 7

            .= (((r4 * (r2 " )) * r2) * ((((r2 " ) * r1) * w1) + w2))

            .= ((r4 * (r2 " )) * (r2 * ((((r2 " ) * r1) * w1) + w2))) by RLVECT_1:def 7

            .= ((r4 * (r2 " )) * ((r2 * (((r2 " ) * r1) * w1)) + (r2 * w2))) by RLVECT_1:def 5

            .= ((r4 * (r2 " )) * (((r2 * ((r2 " ) * r1)) * w1) + (r2 * w2))) by RLVECT_1:def 7

            .= ((r4 * (r2 " )) * ((((r2 * (r2 " )) * r1) * w1) + (r2 * w2)))

            .= ((r4 * (r2 " )) * (((1 * r1) * w1) + (r2 * w2))) by A10, XCMPLX_0:def 7

            .= ((r4 * (r2 " )) * ((r1 * w1) + (r2 * w2)));

            hence contradiction by A1, A2, A5, RLVECT_3: 12;

          end;

        end;

        hence contradiction;

      end;

      then

       A11: ((r1 * r4) - (r2 * r3)) <> 0 ;

       A12:

      now

        assume

         A13: r2 <> 0 ;

        ((r2 " ) * v1) = (((r2 " ) * (r1 * w1)) + ((r2 " ) * (r2 * w2))) by A5, RLVECT_1:def 5

        .= ((((r2 " ) * r1) * w1) + ((r2 " ) * (r2 * w2))) by RLVECT_1:def 7

        .= ((((r2 " ) * r1) * w1) + (((r2 " ) * r2) * w2)) by RLVECT_1:def 7

        .= ((((r2 " ) * r1) * w1) + (1 * w2)) by A13, XCMPLX_0:def 7

        .= ((((r2 " ) * r1) * w1) + w2) by RLVECT_1:def 8;

        then

         A14: w2 = (((r2 " ) * v1) - (((r2 " ) * r1) * w1)) by RLSUB_2: 61;

        then w2 = (((r2 " ) * v1) - ((r2 " ) * (r1 * w1))) by RLVECT_1:def 7;

        

        then v2 = ((r3 * w1) + (r4 * ((r2 " ) * (v1 - (r1 * w1))))) by A6, RLVECT_1: 34

        .= ((r3 * w1) + ((r4 * (r2 " )) * (v1 - (r1 * w1)))) by RLVECT_1:def 7

        .= ((r3 * w1) + (((r4 * (r2 " )) * v1) - ((r4 * (r2 " )) * (r1 * w1)))) by RLVECT_1: 34

        .= (((r3 * w1) + ((r4 * (r2 " )) * v1)) - ((r4 * (r2 " )) * (r1 * w1))) by RLVECT_1:def 3

        .= ((((r4 * (r2 " )) * v1) + (r3 * w1)) - (((r4 * (r2 " )) * r1) * w1)) by RLVECT_1:def 7

        .= (((r4 * (r2 " )) * v1) + ((r3 * w1) - (((r4 * (r2 " )) * r1) * w1))) by RLVECT_1:def 3

        .= (((r4 * (r2 " )) * v1) + ((r3 - ((r4 * (r2 " )) * r1)) * w1)) by RLVECT_1: 35;

        

        then (r2 * v2) = ((r2 * ((r4 * (r2 " )) * v1)) + (r2 * ((r3 - ((r4 * (r2 " )) * r1)) * w1))) by RLVECT_1:def 5

        .= (((r2 * (r4 * (r2 " ))) * v1) + (r2 * ((r3 - ((r4 * (r2 " )) * r1)) * w1))) by RLVECT_1:def 7

        .= (((r4 * (r2 * (r2 " ))) * v1) + (r2 * ((r3 - ((r4 * (r2 " )) * r1)) * w1)))

        .= (((r4 * 1) * v1) + (r2 * ((r3 - ((r4 * (r2 " )) * r1)) * w1))) by A13, XCMPLX_0:def 7

        .= ((r4 * v1) + ((r2 * (r3 - ((r4 * (r2 " )) * r1))) * w1)) by RLVECT_1:def 7

        .= ((r4 * v1) + (((r2 * r3) - ((r2 * (r2 " )) * (r4 * r1))) * w1))

        .= ((r4 * v1) + (((r2 * r3) - (1 * (r4 * r1))) * w1)) by A13, XCMPLX_0:def 7

        .= ((r4 * v1) + (( - t) * w1))

        .= ((r4 * v1) + ( - (t * w1))) by RLVECT_4: 3;

        then ( - (t * w1)) = ((r2 * v2) - (r4 * v1)) by RLSUB_2: 61;

        

        then (t * w1) = ( - ((r2 * v2) - (r4 * v1))) by RLVECT_1: 17

        .= ((r4 * v1) + ( - (r2 * v2))) by RLVECT_1: 33;

        then (((t " ) * t) * w1) = ((t " ) * ((r4 * v1) + ( - (r2 * v2)))) by RLVECT_1:def 7;

        then (1 * w1) = ((t " ) * ((r4 * v1) + ( - (r2 * v2)))) by A11, XCMPLX_0:def 7;

        

        then w1 = ((t " ) * ((r4 * v1) + ( - (r2 * v2)))) by RLVECT_1:def 8

        .= (((t " ) * (r4 * v1)) + ((t " ) * ( - (r2 * v2)))) by RLVECT_1:def 5

        .= ((((t " ) * r4) * v1) + ((t " ) * ( - (r2 * v2)))) by RLVECT_1:def 7

        .= ((((t " ) * r4) * v1) + ((t " ) * (( - r2) * v2))) by RLVECT_4: 3

        .= ((((t " ) * r4) * v1) + (((t " ) * ( - r2)) * v2)) by RLVECT_1:def 7

        .= ((((t " ) * r4) * v1) + ((( - (t " )) * r2) * v2))

        .= ((((t " ) * r4) * v1) + (( - (t " )) * (r2 * v2))) by RLVECT_1:def 7

        .= ((((t " ) * r4) * v1) + ( - ((t " ) * (r2 * v2)))) by RLVECT_4: 3;

        hence w1 = ((((t " ) * r4) * v1) + ( - (((t " ) * r2) * v2))) by RLVECT_1:def 7;

        

        then

         A15: w2 = (((r2 " ) * v1) - (((r2 " ) * r1) * (((t " ) * (r4 * v1)) - (((t " ) * r2) * v2)))) by A14, RLVECT_1:def 7

        .= (((r2 " ) * v1) - (((r2 " ) * r1) * (((t " ) * (r4 * v1)) - ((t " ) * (r2 * v2))))) by RLVECT_1:def 7

        .= (((r2 " ) * v1) - (((r2 " ) * r1) * ((t " ) * ((r4 * v1) - (r2 * v2))))) by RLVECT_1: 34

        .= (((r2 " ) * v1) - (((r1 * (r2 " )) * (t " )) * ((r4 * v1) - (r2 * v2)))) by RLVECT_1:def 7

        .= (((r2 " ) * v1) - ((r1 * ((t " ) * (r2 " ))) * ((r4 * v1) - (r2 * v2))))

        .= (((r2 " ) * v1) - (r1 * (((t " ) * (r2 " )) * ((r4 * v1) - (r2 * v2))))) by RLVECT_1:def 7

        .= (((r2 " ) * v1) - (r1 * ((t " ) * ((r2 " ) * ((r4 * v1) - (r2 * v2)))))) by RLVECT_1:def 7

        .= (((r2 " ) * v1) - (r1 * ((t " ) * (((r2 " ) * (r4 * v1)) - ((r2 " ) * (r2 * v2)))))) by RLVECT_1: 34

        .= (((r2 " ) * v1) - (r1 * ((t " ) * (((r2 " ) * (r4 * v1)) - (((r2 " ) * r2) * v2))))) by RLVECT_1:def 7

        .= (((r2 " ) * v1) - (r1 * ((t " ) * ((((r2 " ) * r4) * v1) - (((r2 " ) * r2) * v2))))) by RLVECT_1:def 7

        .= (((r2 " ) * v1) - (r1 * ((t " ) * ((((r2 " ) * r4) * v1) - (1 * v2))))) by A13, XCMPLX_0:def 7

        .= (((r2 " ) * v1) - (r1 * ((t " ) * ((((r2 " ) * r4) * v1) - v2)))) by RLVECT_1:def 8

        .= (((r2 " ) * v1) - (r1 * (((t " ) * (((r2 " ) * r4) * v1)) - ((t " ) * v2)))) by RLVECT_1: 34

        .= (((r2 " ) * v1) - ((r1 * ((t " ) * (((r2 " ) * r4) * v1))) - (r1 * ((t " ) * v2)))) by RLVECT_1: 34

        .= ((((r2 " ) * v1) - (r1 * ((t " ) * (((r2 " ) * r4) * v1)))) + (r1 * ((t " ) * v2))) by RLVECT_1: 29

        .= ((((r2 " ) * v1) - (r1 * ((t " ) * (((r2 " ) * r4) * v1)))) + ((r1 * (t " )) * v2)) by RLVECT_1:def 7

        .= ((((r2 " ) * v1) - ((r1 * (t " )) * (((r2 " ) * r4) * v1))) + ((r1 * (t " )) * v2)) by RLVECT_1:def 7

        .= ((((r2 " ) * v1) - (((r1 * (t " )) * ((r2 " ) * r4)) * v1)) + ((r1 * (t " )) * v2)) by RLVECT_1:def 7

        .= ((((r2 " ) - ((r1 * (t " )) * ((r2 " ) * r4))) * v1) + (((t " ) * r1) * v2)) by RLVECT_1: 35;

        ((r2 " ) - ((r1 * (t " )) * ((r2 " ) * r4))) = ((r2 " ) * (1 - (r1 * ((t " ) * r4))))

        .= ((r2 " ) * (((t " ) * t) - ((t " ) * (r1 * r4)))) by A11, XCMPLX_0:def 7

        .= ((((r2 " ) * r2) * (t " )) * ( - r3))

        .= ((1 * (t " )) * ( - r3)) by A13, XCMPLX_0:def 7

        .= ( - ((t " ) * r3));

        hence w2 = (( - (((t " ) * r3) * v1)) + (((t " ) * r1) * v2)) by A15, RLVECT_4: 3;

      end;

      set a4 = ((t " ) * r1);

      set a3 = ( - ((t " ) * r3));

      set a2 = ( - ((t " ) * r2));

      set a1 = ((t " ) * r4);

      now

        assume

         A16: r1 <> 0 ;

        

         A17: ((r1 " ) + ((((t " ) * r2) * (r1 " )) * r3)) = ((r1 " ) * (1 + ((t " ) * (r2 * r3))))

        .= ((r1 " ) * (((t " ) * t) + ((t " ) * (r2 * r3)))) by A11, XCMPLX_0:def 7

        .= ((t " ) * (((r1 " ) * r1) * r4))

        .= ((t " ) * (1 * r4)) by A16, XCMPLX_0:def 7

        .= ((t " ) * r4);

        ((r1 " ) * v1) = (((r1 " ) * (r1 * w1)) + ((r1 " ) * (r2 * w2))) by A5, RLVECT_1:def 5

        .= ((((r1 " ) * r1) * w1) + ((r1 " ) * (r2 * w2))) by RLVECT_1:def 7

        .= ((1 * w1) + ((r1 " ) * (r2 * w2))) by A16, XCMPLX_0:def 7

        .= (w1 + ((r1 " ) * (r2 * w2))) by RLVECT_1:def 8

        .= (w1 + ((r2 * (r1 " )) * w2)) by RLVECT_1:def 7;

        then

         A18: w1 = (((r1 " ) * v1) - ((r2 * (r1 " )) * w2)) by RLSUB_2: 61;

        

        then v2 = (((r3 * ((r1 " ) * v1)) - (r3 * ((r2 * (r1 " )) * w2))) + (r4 * w2)) by A6, RLVECT_1: 34

        .= ((((r3 * (r1 " )) * v1) - (r3 * (((r1 " ) * r2) * w2))) + (r4 * w2)) by RLVECT_1:def 7

        .= ((((r3 * (r1 " )) * v1) - ((r3 * ((r1 " ) * r2)) * w2)) + (r4 * w2)) by RLVECT_1:def 7

        .= ((((r3 * (r1 " )) * v1) - (((r1 " ) * (r3 * r2)) * w2)) + (r4 * w2))

        .= (((((r1 " ) * r3) * v1) - ((r1 " ) * ((r3 * r2) * w2))) + (r4 * w2)) by RLVECT_1:def 7

        .= ((((r1 " ) * (r3 * v1)) - ((r1 " ) * ((r3 * r2) * w2))) + (r4 * w2)) by RLVECT_1:def 7;

        

        then (r1 * v2) = ((r1 * (((r1 " ) * (r3 * v1)) - ((r1 " ) * ((r3 * r2) * w2)))) + (r1 * (r4 * w2))) by RLVECT_1:def 5

        .= ((r1 * (((r1 " ) * (r3 * v1)) - ((r1 " ) * ((r3 * r2) * w2)))) + ((r1 * r4) * w2)) by RLVECT_1:def 7

        .= (((r1 * ((r1 " ) * (r3 * v1))) - (r1 * ((r1 " ) * ((r3 * r2) * w2)))) + ((r1 * r4) * w2)) by RLVECT_1: 34

        .= ((((r1 * (r1 " )) * (r3 * v1)) - (r1 * ((r1 " ) * ((r3 * r2) * w2)))) + ((r1 * r4) * w2)) by RLVECT_1:def 7

        .= ((((r1 * (r1 " )) * (r3 * v1)) - ((r1 * (r1 " )) * ((r3 * r2) * w2))) + ((r1 * r4) * w2)) by RLVECT_1:def 7

        .= (((1 * (r3 * v1)) - ((r1 * (r1 " )) * ((r3 * r2) * w2))) + ((r1 * r4) * w2)) by A16, XCMPLX_0:def 7

        .= (((1 * (r3 * v1)) - (1 * ((r3 * r2) * w2))) + ((r1 * r4) * w2)) by A16, XCMPLX_0:def 7

        .= (((r3 * v1) - (1 * ((r3 * r2) * w2))) + ((r1 * r4) * w2)) by RLVECT_1:def 8

        .= (((r3 * v1) - ((r3 * r2) * w2)) + ((r1 * r4) * w2)) by RLVECT_1:def 8

        .= ((r3 * v1) - (((r3 * r2) * w2) - ((r1 * r4) * w2))) by RLVECT_1: 29

        .= ((r3 * v1) + ( - (((r3 * r2) - (r1 * r4)) * w2))) by RLVECT_1: 35

        .= ((r3 * v1) + (( - ((r3 * r2) - (r1 * r4))) * w2)) by RLVECT_4: 3

        .= ((r3 * v1) + (t * w2));

        

        then ((t " ) * (r1 * v2)) = (((t " ) * (r3 * v1)) + ((t " ) * (t * w2))) by RLVECT_1:def 5

        .= (((t " ) * (r3 * v1)) + (((t " ) * t) * w2)) by RLVECT_1:def 7

        .= (((t " ) * (r3 * v1)) + (1 * w2)) by A11, XCMPLX_0:def 7

        .= (((t " ) * (r3 * v1)) + w2) by RLVECT_1:def 8;

        

        hence w2 = (((t " ) * (r1 * v2)) - ((t " ) * (r3 * v1))) by RLSUB_2: 61

        .= ((((t " ) * r1) * v2) - ((t " ) * (r3 * v1))) by RLVECT_1:def 7

        .= (( - (((t " ) * r3) * v1)) + (((t " ) * r1) * v2)) by RLVECT_1:def 7;

        

        hence w1 = (((r1 " ) * v1) - (((r2 * (r1 " )) * ( - (((t " ) * r3) * v1))) + ((r2 * (r1 " )) * (((t " ) * r1) * v2)))) by A18, RLVECT_1:def 5

        .= (((r1 " ) * v1) - (((r2 * (r1 " )) * ( - (((t " ) * r3) * v1))) + (((r2 * (r1 " )) * ((t " ) * r1)) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - (((r2 * (r1 " )) * ( - (((t " ) * r3) * v1))) + ((r2 * (((r1 " ) * r1) * (t " ))) * v2)))

        .= (((r1 " ) * v1) - (((r2 * (r1 " )) * ( - (((t " ) * r3) * v1))) + ((r2 * (1 * (t " ))) * v2))) by A16, XCMPLX_0:def 7

        .= (((r1 " ) * v1) - (((r2 * (r1 " )) * ( - ((t " ) * (r3 * v1)))) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - (((r2 * (r1 " )) * (( - (t " )) * (r3 * v1))) + ((r2 * (t " )) * v2))) by RLVECT_4: 3

        .= (((r1 " ) * v1) - ((((r2 * (r1 " )) * ( - (t " ))) * (r3 * v1)) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - (((((( - jj) * (t " )) * r2) * (r1 " )) * (r3 * v1)) + ((r2 * (t " )) * v2)))

        .= (((r1 " ) * v1) - ((((( - jj) * (t " )) * r2) * ((r1 " ) * (r3 * v1))) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - (((( - jj) * (t " )) * (r2 * ((r1 " ) * (r3 * v1)))) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - ((( - jj) * ((t " ) * (r2 * ((r1 " ) * (r3 * v1))))) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - (( - ((t " ) * (r2 * ((r1 " ) * (r3 * v1))))) + ((r2 * (t " )) * v2))) by RLVECT_1: 16

        .= (((r1 " ) * v1) - (( - (((t " ) * r2) * ((r1 " ) * (r3 * v1)))) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - (( - ((((t " ) * r2) * (r1 " )) * (r3 * v1))) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - (( - (((((t " ) * r2) * (r1 " )) * r3) * v1)) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= ((((r1 " ) * v1) - ( - (((((t " ) * r2) * (r1 " )) * r3) * v1))) - ((r2 * (t " )) * v2)) by RLVECT_1: 27

        .= ((((r1 " ) * v1) + (((((t " ) * r2) * (r1 " )) * r3) * v1)) - ((r2 * (t " )) * v2)) by RLVECT_1: 17

        .= ((((t " ) * r4) * v1) + ( - (((t " ) * r2) * v2))) by A17, RLVECT_1:def 6;

      end;

      then

       A19: w1 = ((((t " ) * r4) * v1) + (( - ((t " ) * r2)) * v2)) & w2 = ((( - ((t " ) * r3)) * v1) + (((t " ) * r1) * v2)) by A7, A12, RLVECT_4: 3;

      now

        let u be VECTOR of V;

        thus u in ( Lin {w1, w2}) implies u in ( Lin {v1, v2})

        proof

          assume u in ( Lin {w1, w2});

          then

          consider r5,r6 be Real such that

           A20: u = ((r5 * w1) + (r6 * w2)) by Th32;

          u = (((r5 * (a1 * v1)) + (r5 * (a2 * v2))) + (r6 * ((a3 * v1) + (a4 * v2)))) by A19, A20, RLVECT_1:def 5

          .= (((r5 * (a1 * v1)) + (r5 * (a2 * v2))) + ((r6 * (a3 * v1)) + (r6 * (a4 * v2)))) by RLVECT_1:def 5

          .= ((((r5 * a1) * v1) + (r5 * (a2 * v2))) + ((r6 * (a3 * v1)) + (r6 * (a4 * v2)))) by RLVECT_1:def 7

          .= ((((r5 * a1) * v1) + ((r5 * a2) * v2)) + ((r6 * (a3 * v1)) + (r6 * (a4 * v2)))) by RLVECT_1:def 7

          .= ((((r5 * a1) * v1) + ((r5 * a2) * v2)) + (((r6 * a3) * v1) + (r6 * (a4 * v2)))) by RLVECT_1:def 7

          .= ((((r5 * a1) * v1) + ((r5 * a2) * v2)) + (((r6 * a3) * v1) + ((r6 * a4) * v2))) by RLVECT_1:def 7

          .= (((r5 * a1) * v1) + (((r5 * a2) * v2) + (((r6 * a3) * v1) + ((r6 * a4) * v2)))) by RLVECT_1:def 3

          .= (((r5 * a1) * v1) + (((r6 * a3) * v1) + (((r5 * a2) * v2) + ((r6 * a4) * v2)))) by RLVECT_1:def 3

          .= ((((r5 * a1) * v1) + ((r6 * a3) * v1)) + (((r5 * a2) * v2) + ((r6 * a4) * v2))) by RLVECT_1:def 3

          .= ((((r5 * a1) + (r6 * a3)) * v1) + (((r5 * a2) * v2) + ((r6 * a4) * v2))) by RLVECT_1:def 6

          .= ((((r5 * a1) + (r6 * a3)) * v1) + (((r5 * a2) + (r6 * a4)) * v2)) by RLVECT_1:def 6;

          hence thesis by Th32;

        end;

        assume u in ( Lin {v1, v2});

        then

        consider r5,r6 be Real such that

         A21: u = ((r5 * v1) + (r6 * v2)) by Th32;

        u = ((r5 * ((r1 * w1) + (r2 * w2))) + ((r6 * (r3 * w1)) + (r6 * (r4 * w2)))) by A5, A6, A21, RLVECT_1:def 5

        .= (((r5 * (r1 * w1)) + (r5 * (r2 * w2))) + ((r6 * (r3 * w1)) + (r6 * (r4 * w2)))) by RLVECT_1:def 5

        .= ((((r5 * (r1 * w1)) + (r5 * (r2 * w2))) + (r6 * (r3 * w1))) + (r6 * (r4 * w2))) by RLVECT_1:def 3

        .= ((((r5 * (r1 * w1)) + (r6 * (r3 * w1))) + (r5 * (r2 * w2))) + (r6 * (r4 * w2))) by RLVECT_1:def 3

        .= (((((r5 * r1) * w1) + (r6 * (r3 * w1))) + (r5 * (r2 * w2))) + (r6 * (r4 * w2))) by RLVECT_1:def 7

        .= (((((r5 * r1) * w1) + ((r6 * r3) * w1)) + (r5 * (r2 * w2))) + (r6 * (r4 * w2))) by RLVECT_1:def 7

        .= (((((r5 * r1) * w1) + ((r6 * r3) * w1)) + ((r5 * r2) * w2)) + (r6 * (r4 * w2))) by RLVECT_1:def 7

        .= (((((r5 * r1) * w1) + ((r6 * r3) * w1)) + ((r5 * r2) * w2)) + ((r6 * r4) * w2)) by RLVECT_1:def 7

        .= (((((r5 * r1) + (r6 * r3)) * w1) + ((r5 * r2) * w2)) + ((r6 * r4) * w2)) by RLVECT_1:def 6

        .= ((((r5 * r1) + (r6 * r3)) * w1) + (((r5 * r2) * w2) + ((r6 * r4) * w2))) by RLVECT_1:def 3

        .= ((((r5 * r1) + (r6 * r3)) * w1) + (((r5 * r2) + (r6 * r4)) * w2)) by RLVECT_1:def 6;

        hence u in ( Lin {w1, w2}) by Th32;

      end;

      hence ( Lin {w1, w2}) = ( Lin {v1, v2}) by RUSUB_1: 25;

      now

        let a,b be Real;

        

         A22: (t " ) <> 0 by A11, XCMPLX_1: 202;

        assume ((a * w1) + (b * w2)) = ( 0. V);

        

        then

         A23: ( 0. V) = (((a * (a1 * v1)) + (a * (a2 * v2))) + (b * ((a3 * v1) + (a4 * v2)))) by A19, RLVECT_1:def 5

        .= (((a * (a1 * v1)) + (a * (a2 * v2))) + ((b * (a3 * v1)) + (b * (a4 * v2)))) by RLVECT_1:def 5

        .= ((((a * a1) * v1) + (a * (a2 * v2))) + ((b * (a3 * v1)) + (b * (a4 * v2)))) by RLVECT_1:def 7

        .= ((((a * a1) * v1) + (a * (a2 * v2))) + ((b * (a3 * v1)) + ((b * a4) * v2))) by RLVECT_1:def 7

        .= ((((a * a1) * v1) + (a * (a2 * v2))) + (((b * a3) * v1) + ((b * a4) * v2))) by RLVECT_1:def 7

        .= ((((a * a1) * v1) + ((a * a2) * v2)) + (((b * a3) * v1) + ((b * a4) * v2))) by RLVECT_1:def 7

        .= (((a * a1) * v1) + (((a * a2) * v2) + (((b * a3) * v1) + ((b * a4) * v2)))) by RLVECT_1:def 3

        .= (((a * a1) * v1) + (((b * a3) * v1) + (((a * a2) * v2) + ((b * a4) * v2)))) by RLVECT_1:def 3

        .= ((((a * a1) * v1) + ((b * a3) * v1)) + (((a * a2) * v2) + ((b * a4) * v2))) by RLVECT_1:def 3

        .= ((((a * a1) + (b * a3)) * v1) + (((a * a2) * v2) + ((b * a4) * v2))) by RLVECT_1:def 6

        .= ((((a * a1) + (b * a3)) * v1) + (((a * a2) + (b * a4)) * v2)) by RLVECT_1:def 6;

        then 0 = ((t " ) * ((r4 * a) + (( - r3) * b))) by A1, A2, RLVECT_3: 13;

        then

         A24: ((r4 * a) - (r3 * b)) = 0 by A22, XCMPLX_1: 6;

         0 = ((t " ) * ((( - r2) * a) + (r1 * b))) by A1, A2, A23, RLVECT_3: 13;

        then

         A25: ((r1 * b) + ( - (r2 * a))) = 0 by A22, XCMPLX_1: 6;

        assume

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

        now

          per cases by A26;

            suppose

             A27: a <> 0 ;

            ((a " ) * (r1 * b)) = (((a " ) * a) * r2) by A25, XCMPLX_1: 4;

            then ((a " ) * (r1 * b)) = (1 * r2) by A27, XCMPLX_0:def 7;

            then r2 = (r1 * ((a " ) * b));

            then v1 = ((r1 * w1) + (r1 * (((a " ) * b) * w2))) by A5, RLVECT_1:def 7;

            then

             A28: v1 = (r1 * (w1 + (((a " ) * b) * w2))) by RLVECT_1:def 5;

            (((a " ) * a) * r4) = ((a " ) * (r3 * b)) by A24, XCMPLX_1: 4;

            then (1 * r4) = ((a " ) * (r3 * b)) by A27, XCMPLX_0:def 7;

            then r4 = (r3 * ((a " ) * b));

            then v2 = ((r3 * w1) + (r3 * (((a " ) * b) * w2))) by A6, RLVECT_1:def 7;

            then v2 = (r3 * (w1 + (((a " ) * b) * w2))) by RLVECT_1:def 5;

            hence contradiction by A1, A2, A28, RLVECT_4: 21;

          end;

            suppose

             A29: b <> 0 ;

            (((b " ) * b) * r1) = ((b " ) * (r2 * a)) by A25, XCMPLX_1: 4;

            then (1 * r1) = ((b " ) * (r2 * a)) by A29, XCMPLX_0:def 7;

            then r1 = (r2 * ((b " ) * a));

            then v1 = ((r2 * (((b " ) * a) * w1)) + (r2 * w2)) by A5, RLVECT_1:def 7;

            then

             A30: v1 = (r2 * ((((b " ) * a) * w1) + w2)) by RLVECT_1:def 5;

            (((b " ) * b) * r3) = ((b " ) * (r4 * a)) by A24, XCMPLX_1: 4;

            then (1 * r3) = ((b " ) * (r4 * a)) by A29, XCMPLX_0:def 7;

            then r3 = (r4 * ((b " ) * a));

            then v2 = ((r4 * (((b " ) * a) * w1)) + (r4 * w2)) by A6, RLVECT_1:def 7;

            then v2 = (r4 * ((((b " ) * a) * w1) + w2)) by RLVECT_1:def 5;

            hence contradiction by A1, A2, A30, RLVECT_4: 21;

          end;

        end;

        hence contradiction;

      end;

      hence thesis by RLVECT_3: 13;

    end;

    begin

    theorem :: RUSUB_3:40

    for V be RealUnitarySpace, x be set holds x in ( (0). V) iff x = ( 0. V) by Lm1;

    theorem :: RUSUB_3:41

    for V be RealUnitarySpace, W1,W2,W3 be Subspace of V st W1 is Subspace of W3 holds (W1 /\ W2) is Subspace of W3 by Lm2;

    theorem :: RUSUB_3:42

    for V be RealUnitarySpace, W1,W2,W3 be Subspace of V st W1 is Subspace of W2 & W1 is Subspace of W3 holds W1 is Subspace of (W2 /\ W3) by Lm3;

    theorem :: RUSUB_3:43

    for V be RealUnitarySpace, W1,W2,W3 be Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds (W1 + W2) is Subspace of W3 by Lm5;

    theorem :: RUSUB_3:44

    for V be RealUnitarySpace, W1,W2,W3 be Subspace of V st W1 is Subspace of W2 holds W1 is Subspace of (W2 + W3) by Lm4;

    theorem :: RUSUB_3:45

    for V be RealUnitarySpace, W1,W2 be Subspace of V, v be VECTOR of V st W1 is Subspace of W2 holds (v + W1) c= (v + W2)

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      let v be VECTOR of V;

      assume

       A1: W1 is Subspace of W2;

      let x be object;

      assume x in (v + W1);

      then

      consider u be VECTOR of V such that

       A2: u in W1 and

       A3: x = (v + u) by RUSUB_2: 63;

      u in W2 by A1, A2, RUSUB_1: 1;

      hence thesis by A3, RUSUB_2: 63;

    end;