rusub_2.miz



    begin

    definition

      let V be RealUnitarySpace, W1,W2 be Subspace of V;

      :: RUSUB_2:def1

      func W1 + W2 -> strict Subspace of V means

      : Def1: the carrier of it = { (v + u) where v,u be VECTOR of V : v in W1 & u in W2 };

      existence

      proof

        reconsider V1 = the carrier of W1, V2 = the carrier of W2 as Subset of V by RUSUB_1:def 1;

        set VS = { (v + u) where v,u be VECTOR of V : v in W1 & u in W2 };

        VS c= the carrier of V

        proof

          let x be object;

          assume x in VS;

          then ex v1,v2 be VECTOR of V st x = (v1 + v2) & v1 in W1 & v2 in W2;

          hence thesis;

        end;

        then

        reconsider VS as Subset of V;

        

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

        ( 0. V) in W1 & ( 0. V) in W2 by RUSUB_1: 11;

        then

         A2: ( 0. V) in VS by A1;

        

         A3: VS = { (v + u) where u,v be VECTOR of V : v in V1 & u in V2 }

        proof

          thus VS c= { (v + u) where u,v be VECTOR of V : v in V1 & u in V2 }

          proof

            let x be object;

            assume x in VS;

            then

            consider v,u be VECTOR of V such that

             A4: x = (v + u) and

             A5: v in W1 & u in W2;

            v in V1 & u in V2 by A5, STRUCT_0:def 5;

            hence thesis by A4;

          end;

          let x be object;

          assume x in { (v + u) where u,v be VECTOR of V : v in V1 & u in V2 };

          then

          consider u,v be VECTOR of V such that

           A6: x = (v + u) and

           A7: v in V1 & u in V2;

          v in W1 & u in W2 by A7, STRUCT_0:def 5;

          hence thesis by A6;

        end;

        V1 is linearly-closed & V2 is linearly-closed by RUSUB_1: 28;

        hence thesis by A2, A3, RLSUB_1: 6, RUSUB_1: 29;

      end;

      uniqueness by RUSUB_1: 24;

    end

    definition

      let V be RealUnitarySpace, W1,W2 be Subspace of V;

      :: RUSUB_2:def2

      func W1 /\ W2 -> strict Subspace of V means

      : Def2: the carrier of it = (the carrier of W1 /\ the carrier of W2);

      existence

      proof

        set VW2 = the carrier of W2;

        set VW1 = the carrier of W1;

        set VV = the carrier of V;

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

        then

         A1: ( 0. V) in VW2 by STRUCT_0:def 5;

        VW1 c= VV & VW2 c= VV by RUSUB_1:def 1;

        then (VW1 /\ VW2) c= (VV /\ VV) by XBOOLE_1: 27;

        then

        reconsider V1 = VW1, V2 = VW2, V3 = (VW1 /\ VW2) as Subset of V by RUSUB_1:def 1;

        V1 is linearly-closed & V2 is linearly-closed by RUSUB_1: 28;

        then

         A2: V3 is linearly-closed by RLSUB_1: 7;

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

        then ( 0. V) in VW1 by STRUCT_0:def 5;

        then (VW1 /\ VW2) <> {} by A1, XBOOLE_0:def 4;

        hence thesis by A2, RUSUB_1: 29;

      end;

      uniqueness by RUSUB_1: 24;

    end

    begin

    theorem :: RUSUB_2:1

    

     Th1: for V be RealUnitarySpace, W1,W2 be Subspace of V, x be object holds x in (W1 + W2) iff ex v1,v2 be VECTOR of V st v1 in W1 & v2 in W2 & x = (v1 + v2)

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      let x be object;

      thus x in (W1 + W2) implies ex v1,v2 be VECTOR of V st v1 in W1 & v2 in W2 & x = (v1 + v2)

      proof

        assume x in (W1 + W2);

        then x in the carrier of (W1 + W2) by STRUCT_0:def 5;

        then x in { (v + u) where v,u be VECTOR of V : v in W1 & u in W2 } by Def1;

        then

        consider v1,v2 be VECTOR of V such that

         A1: x = (v1 + v2) & v1 in W1 & v2 in W2;

        take v1, v2;

        thus thesis by A1;

      end;

      given v1,v2 be VECTOR of V such that

       A2: v1 in W1 & v2 in W2 & x = (v1 + v2);

      x in { (v + u) where v,u be VECTOR of V : v in W1 & u in W2 } by A2;

      then x in the carrier of (W1 + W2) by Def1;

      hence thesis by STRUCT_0:def 5;

    end;

    theorem :: RUSUB_2:2

    

     Th2: for V be RealUnitarySpace, W1,W2 be Subspace of V, v be VECTOR of V st v in W1 or v in W2 holds v in (W1 + W2)

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      let v be VECTOR of V;

      assume

       A1: v in W1 or v in W2;

      now

        per cases by A1;

          suppose

           A2: v in W1;

          v = (v + ( 0. V)) & ( 0. V) in W2 by RLVECT_1: 4, RUSUB_1: 11;

          hence thesis by A2, Th1;

        end;

          suppose

           A3: v in W2;

          v = (( 0. V) + v) & ( 0. V) in W1 by RLVECT_1: 4, RUSUB_1: 11;

          hence thesis by A3, Th1;

        end;

      end;

      hence thesis;

    end;

    theorem :: RUSUB_2:3

    

     Th3: for V be RealUnitarySpace, W1,W2 be Subspace of V, x be object holds x in (W1 /\ W2) iff x in W1 & x in W2

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      let x be object;

      x in (W1 /\ W2) iff x in the carrier of (W1 /\ W2) by STRUCT_0:def 5;

      then x in (W1 /\ W2) iff x in (the carrier of W1 /\ the carrier of W2) by Def2;

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

      hence thesis by STRUCT_0:def 5;

    end;

    

     Lm1: for V be RealUnitarySpace, W1,W2 be Subspace of V holds (W1 + W2) = (W2 + W1)

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      set A = { (v + u) where v,u be VECTOR of V : v in W1 & u in W2 };

      set B = { (v + u) where v,u be VECTOR of V : v in W2 & u in W1 };

      

       A1: B c= A

      proof

        let x be object;

        assume x in B;

        then ex v,u be VECTOR of V st x = (v + u) & v in W2 & u in W1;

        hence thesis;

      end;

      

       A2: the carrier of (W1 + W2) = A by Def1;

      A c= B

      proof

        let x be object;

        assume x in A;

        then ex v,u be VECTOR of V st x = (v + u) & v in W1 & u in W2;

        hence thesis;

      end;

      then A = B by A1;

      hence thesis by A2, Def1;

    end;

    

     Lm2: for V be RealUnitarySpace, W1,W2 be Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2)

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      let x be object;

      set A = { (v + u) where v,u be VECTOR of V : v in W1 & u in W2 };

      assume x in the carrier of W1;

      then

      reconsider v = x as Element of W1;

      reconsider v as VECTOR of V by RUSUB_1: 3;

      

       A1: v = (v + ( 0. V)) by RLVECT_1: 4;

      v in W1 & ( 0. V) in W2 by RUSUB_1: 11, STRUCT_0:def 5;

      then x in A by A1;

      hence thesis by Def1;

    end;

    

     Lm3: for V be RealUnitarySpace, W1 be Subspace of V, W2 be strict Subspace of V st the carrier of W1 c= the carrier of W2 holds (W1 + W2) = W2

    proof

      let V be RealUnitarySpace;

      let W1 be Subspace of V;

      let W2 be strict Subspace of V;

      assume

       A1: the carrier of W1 c= the carrier of W2;

      

       A2: the carrier of (W1 + W2) c= the carrier of W2

      proof

        let x be object;

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

        then x in { (v + u) where v,u be VECTOR of V : v in W1 & u in W2 } by Def1;

        then

        consider v,u be VECTOR of V such that

         A3: x = (v + u) and

         A4: v in W1 and

         A5: u in W2;

        W1 is Subspace of W2 by A1, RUSUB_1: 22;

        then v in W2 by A4, RUSUB_1: 1;

        then (v + u) in W2 by A5, RUSUB_1: 14;

        hence thesis by A3, STRUCT_0:def 5;

      end;

      (W1 + W2) = (W2 + W1) by Lm1;

      then the carrier of W2 c= the carrier of (W1 + W2) by Lm2;

      then the carrier of (W1 + W2) = the carrier of W2 by A2;

      hence thesis by RUSUB_1: 24;

    end;

    theorem :: RUSUB_2:4

    for V be RealUnitarySpace, W be strict Subspace of V holds (W + W) = W by Lm3;

    theorem :: RUSUB_2:5

    for V be RealUnitarySpace, W1,W2 be Subspace of V holds (W1 + W2) = (W2 + W1) by Lm1;

    theorem :: RUSUB_2:6

    

     Th6: for V be RealUnitarySpace, W1,W2,W3 be Subspace of V holds (W1 + (W2 + W3)) = ((W1 + W2) + W3)

    proof

      let V be RealUnitarySpace;

      let W1,W2,W3 be Subspace of V;

      set A = { (v + u) where v,u be VECTOR of V : v in W1 & u in W2 };

      set B = { (v + u) where v,u be VECTOR of V : v in W2 & u in W3 };

      set C = { (v + u) where v,u be VECTOR of V : v in (W1 + W2) & u in W3 };

      set D = { (v + u) where v,u be VECTOR of V : v in W1 & u in (W2 + W3) };

      

       A1: the carrier of (W1 + (W2 + W3)) = D by Def1;

      

       A2: C c= D

      proof

        let x be object;

        assume x in C;

        then

        consider v,u be VECTOR of V such that

         A3: x = (v + u) and

         A4: v in (W1 + W2) and

         A5: u in W3;

        v in the carrier of (W1 + W2) by A4, STRUCT_0:def 5;

        then v in A by Def1;

        then

        consider u1,u2 be VECTOR of V such that

         A6: v = (u1 + u2) and

         A7: u1 in W1 and

         A8: u2 in W2;

        (u2 + u) in B by A5, A8;

        then (u2 + u) in the carrier of (W2 + W3) by Def1;

        then

         A9: (u2 + u) in (W2 + W3) by STRUCT_0:def 5;

        (v + u) = (u1 + (u2 + u)) by A6, RLVECT_1:def 3;

        hence thesis by A3, A7, A9;

      end;

      D c= C

      proof

        let x be object;

        assume x in D;

        then

        consider v,u be VECTOR of V such that

         A10: x = (v + u) and

         A11: v in W1 and

         A12: u in (W2 + W3);

        u in the carrier of (W2 + W3) by A12, STRUCT_0:def 5;

        then u in B by Def1;

        then

        consider u1,u2 be VECTOR of V such that

         A13: u = (u1 + u2) and

         A14: u1 in W2 and

         A15: u2 in W3;

        (v + u1) in A by A11, A14;

        then (v + u1) in the carrier of (W1 + W2) by Def1;

        then

         A16: (v + u1) in (W1 + W2) by STRUCT_0:def 5;

        (v + u) = ((v + u1) + u2) by A13, RLVECT_1:def 3;

        hence thesis by A10, A15, A16;

      end;

      then D = C by A2;

      hence thesis by A1, Def1;

    end;

    theorem :: RUSUB_2:7

    

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

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      the carrier of W1 c= the carrier of (W1 + W2) by Lm2;

      hence W1 is Subspace of (W1 + W2) by RUSUB_1: 22;

      the carrier of W2 c= the carrier of (W2 + W1) by Lm2;

      then the carrier of W2 c= the carrier of (W1 + W2) by Lm1;

      hence thesis by RUSUB_1: 22;

    end;

    theorem :: RUSUB_2:8

    

     Th8: for V be RealUnitarySpace, W1 be Subspace of V, W2 be strict Subspace of V holds W1 is Subspace of W2 iff (W1 + W2) = W2

    proof

      let V be RealUnitarySpace;

      let W1 be Subspace of V;

      let W2 be strict Subspace of V;

      thus W1 is Subspace of W2 implies (W1 + W2) = W2

      proof

        assume W1 is Subspace of W2;

        then the carrier of W1 c= the carrier of W2 by RUSUB_1:def 1;

        hence thesis by Lm3;

      end;

      thus thesis by Th7;

    end;

    theorem :: RUSUB_2:9

    

     Th9: for V be RealUnitarySpace, W be strict Subspace of V holds (( (0). V) + W) = W & (W + ( (0). V)) = W

    proof

      let V be RealUnitarySpace;

      let W be strict Subspace of V;

      ( (0). V) is Subspace of W by RUSUB_1: 33;

      then the carrier of ( (0). V) c= the carrier of W by RUSUB_1:def 1;

      hence (( (0). V) + W) = W by Lm3;

      hence thesis by Lm1;

    end;

    theorem :: RUSUB_2:10

    

     Th10: for V be RealUnitarySpace holds (( (0). V) + ( (Omega). V)) = the UNITSTR of V & (( (Omega). V) + ( (0). V)) = the UNITSTR of V

    proof

      let V be RealUnitarySpace;

      

      thus (( (0). V) + ( (Omega). V)) = ( (Omega). V) by Th9

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

      hence thesis by Lm1;

    end;

    theorem :: RUSUB_2:11

    

     Th11: for V be RealUnitarySpace, W be Subspace of V holds (( (Omega). V) + W) = the UNITSTR of V & (W + ( (Omega). V)) = the UNITSTR of V

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

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

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

      

      then (W + ( (Omega). V)) = ( (Omega). V) by Lm3

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

      hence thesis by Lm1;

    end;

    theorem :: RUSUB_2:12

    for V be strict RealUnitarySpace holds (( (Omega). V) + ( (Omega). V)) = V by Th11;

    theorem :: RUSUB_2:13

    for V be RealUnitarySpace, W be strict Subspace of V holds (W /\ W) = W

    proof

      let V be RealUnitarySpace;

      let W be strict Subspace of V;

      the carrier of W = (the carrier of W /\ the carrier of W);

      hence thesis by Def2;

    end;

    theorem :: RUSUB_2:14

    

     Th14: for V be RealUnitarySpace, W1,W2 be Subspace of V holds (W1 /\ W2) = (W2 /\ W1)

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      the carrier of (W1 /\ W2) = (the carrier of W2 /\ the carrier of W1) by Def2;

      hence thesis by Def2;

    end;

    theorem :: RUSUB_2:15

    

     Th15: for V be RealUnitarySpace, W1,W2,W3 be Subspace of V holds (W1 /\ (W2 /\ W3)) = ((W1 /\ W2) /\ W3)

    proof

      let V be RealUnitarySpace;

      let W1,W2,W3 be Subspace of V;

      set V1 = the carrier of W1;

      set V2 = the carrier of W2;

      set V3 = the carrier of W3;

      the carrier of (W1 /\ (W2 /\ W3)) = (V1 /\ the carrier of (W2 /\ W3)) by Def2

      .= (V1 /\ (V2 /\ V3)) by Def2

      .= ((V1 /\ V2) /\ V3) by XBOOLE_1: 16

      .= (the carrier of (W1 /\ W2) /\ V3) by Def2;

      hence thesis by Def2;

    end;

    

     Lm4: for V be RealUnitarySpace, W1,W2 be Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of W1

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      the carrier of (W1 /\ W2) = (the carrier of W1 /\ the carrier of W2) by Def2;

      hence thesis by XBOOLE_1: 17;

    end;

    theorem :: RUSUB_2:16

    

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

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      the carrier of (W1 /\ W2) c= the carrier of W1 by Lm4;

      hence (W1 /\ W2) is Subspace of W1 by RUSUB_1: 22;

      the carrier of (W2 /\ W1) c= the carrier of W2 by Lm4;

      then the carrier of (W1 /\ W2) c= the carrier of W2 by Th14;

      hence thesis by RUSUB_1: 22;

    end;

    theorem :: RUSUB_2:17

    

     Th17: for V be RealUnitarySpace, W2 be Subspace of V, W1 be strict Subspace of V holds W1 is Subspace of W2 iff (W1 /\ W2) = W1

    proof

      let V be RealUnitarySpace;

      let W2 be Subspace of V;

      let W1 be strict Subspace of V;

      thus W1 is Subspace of W2 implies (W1 /\ W2) = W1

      proof

        assume W1 is Subspace of W2;

        then

         A1: the carrier of W1 c= the carrier of W2 by RUSUB_1:def 1;

        the carrier of (W1 /\ W2) = (the carrier of W1 /\ the carrier of W2) by Def2;

        hence thesis by A1, RUSUB_1: 24, XBOOLE_1: 28;

      end;

      thus thesis by Th16;

    end;

    theorem :: RUSUB_2:18

    

     Th18: for V be RealUnitarySpace, W be Subspace of V holds (( (0). V) /\ W) = ( (0). V) & (W /\ ( (0). V)) = ( (0). V)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

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

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

      then {( 0. V)} c= the carrier of W by ZFMISC_1: 31;

      then

       A1: ( {( 0. V)} /\ the carrier of W) = {( 0. V)} by XBOOLE_1: 28;

      the carrier of (( (0). V) /\ W) = (the carrier of ( (0). V) /\ the carrier of W) by Def2

      .= ( {( 0. V)} /\ the carrier of W) by RUSUB_1:def 2;

      hence (( (0). V) /\ W) = ( (0). V) by A1, RUSUB_1:def 2;

      hence thesis by Th14;

    end;

    theorem :: RUSUB_2:19

    for V be RealUnitarySpace holds (( (0). V) /\ ( (Omega). V)) = ( (0). V) & (( (Omega). V) /\ ( (0). V)) = ( (0). V) by Th18;

    theorem :: RUSUB_2:20

    

     Th20: for V be RealUnitarySpace, W be strict Subspace of V holds (( (Omega). V) /\ W) = W & (W /\ ( (Omega). V)) = W

    proof

      let V be RealUnitarySpace;

      let W be strict Subspace of V;

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

      then

       A1: the carrier of (( (Omega). V) /\ W) = (the carrier of V /\ the carrier of W) by Def2;

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

      hence (( (Omega). V) /\ W) = W by A1, RUSUB_1: 24, XBOOLE_1: 28;

      hence thesis by Th14;

    end;

    theorem :: RUSUB_2:21

    for V be strict RealUnitarySpace holds (( (Omega). V) /\ ( (Omega). V)) = V

    proof

      let V be strict RealUnitarySpace;

      

      thus (( (Omega). V) /\ ( (Omega). V)) = ( (Omega). V) by Th20

      .= V by RUSUB_1:def 3;

    end;

    

     Lm5: for V be RealUnitarySpace, W1,W2 be Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      the carrier of (W1 /\ W2) c= the carrier of W1 & the carrier of W1 c= the carrier of (W1 + W2) by Lm2, Lm4;

      hence thesis;

    end;

    theorem :: RUSUB_2:22

    for V be RealUnitarySpace, W1,W2 be Subspace of V holds (W1 /\ W2) is Subspace of (W1 + W2) by Lm5, RUSUB_1: 22;

    

     Lm6: for V be RealUnitarySpace, W1,W2 be Subspace of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      thus the carrier of ((W1 /\ W2) + W2) c= the carrier of W2

      proof

        let x be object;

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

        then x in { (u + v) where u,v be VECTOR of V : u in (W1 /\ W2) & v in W2 } by Def1;

        then

        consider u,v be VECTOR of V such that

         A1: x = (u + v) and

         A2: u in (W1 /\ W2) and

         A3: v in W2;

        u in W2 by A2, Th3;

        then (u + v) in W2 by A3, RUSUB_1: 14;

        hence thesis by A1, STRUCT_0:def 5;

      end;

      let x be object;

      the carrier of W2 c= the carrier of (W2 + (W1 /\ W2)) by Lm2;

      then

       A4: the carrier of W2 c= the carrier of ((W1 /\ W2) + W2) by Lm1;

      assume x in the carrier of W2;

      hence thesis by A4;

    end;

    theorem :: RUSUB_2:23

    for V be RealUnitarySpace, W1 be Subspace of V, W2 be strict Subspace of V holds ((W1 /\ W2) + W2) = W2 by Lm6, RUSUB_1: 24;

    

     Lm7: for V be RealUnitarySpace, W1,W2 be Subspace of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      thus the carrier of (W1 /\ (W1 + W2)) c= the carrier of W1

      proof

        let x be object;

        assume

         A1: x in the carrier of (W1 /\ (W1 + W2));

        the carrier of (W1 /\ (W1 + W2)) = (the carrier of W1 /\ the carrier of (W1 + W2)) by Def2;

        hence thesis by A1, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A2: x in the carrier of W1;

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

      then

      reconsider x1 = x as Element of V by A2;

      

       A3: (x1 + ( 0. V)) = x1 & ( 0. V) in W2 by RLVECT_1: 4, RUSUB_1: 11;

      x in W1 by A2, STRUCT_0:def 5;

      then x in { (u + v) where u,v be VECTOR of V : u in W1 & v in W2 } by A3;

      then x in the carrier of (W1 + W2) by Def1;

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

      hence thesis by Def2;

    end;

    theorem :: RUSUB_2:24

    for V be RealUnitarySpace, W1 be Subspace of V, W2 be strict Subspace of V holds (W2 /\ (W2 + W1)) = W2 by Lm7, RUSUB_1: 24;

    

     Lm8: for V be RealUnitarySpace, W1,W2,W3 be Subspace of V holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))

    proof

      let V be RealUnitarySpace;

      let W1,W2,W3 be Subspace of V;

      let x be object;

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

      then x in { (u + v) where u,v be VECTOR of V : u in (W1 /\ W2) & v in (W2 /\ W3) } by Def1;

      then

      consider u,v be VECTOR of V such that

       A1: x = (u + v) and

       A2: u in (W1 /\ W2) & v in (W2 /\ W3);

      u in W2 & v in W2 by A2, Th3;

      then

       A3: x in W2 by A1, RUSUB_1: 14;

      u in W1 & v in W3 by A2, Th3;

      then x in (W1 + W3) by A1, Th1;

      then x in (W2 /\ (W1 + W3)) by A3, Th3;

      hence thesis by STRUCT_0:def 5;

    end;

    theorem :: RUSUB_2:25

    for V be RealUnitarySpace, W1,W2,W3 be Subspace of V holds ((W1 /\ W2) + (W2 /\ W3)) is Subspace of (W2 /\ (W1 + W3)) by Lm8, RUSUB_1: 22;

    

     Lm9: for V be RealUnitarySpace, W1,W2,W3 be Subspace of V st W1 is Subspace of W2 holds the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))

    proof

      let V be RealUnitarySpace;

      let W1,W2,W3 be Subspace of V;

      assume

       A1: W1 is Subspace of W2;

      thus the carrier of (W2 /\ (W1 + W3)) c= the carrier of ((W1 /\ W2) + (W2 /\ W3))

      proof

        let x be object;

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

        then

         A2: x in (the carrier of W2 /\ the carrier of (W1 + W3)) by Def2;

        then x in the carrier of (W1 + W3) by XBOOLE_0:def 4;

        then x in { (u + v) where u,v be VECTOR of V : u in W1 & v in W3 } by Def1;

        then

        consider u1,v1 be VECTOR of V such that

         A3: x = (u1 + v1) and

         A4: u1 in W1 and

         A5: v1 in W3;

        

         A6: u1 in W2 by A1, A4, RUSUB_1: 1;

        x in the carrier of W2 by A2, XBOOLE_0:def 4;

        then (u1 + v1) in W2 by A3, STRUCT_0:def 5;

        then ((v1 + u1) - u1) in W2 by A6, RUSUB_1: 17;

        then (v1 + (u1 - u1)) in W2 by RLVECT_1:def 3;

        then (v1 + ( 0. V)) in W2 by RLVECT_1: 15;

        then v1 in W2 by RLVECT_1: 4;

        then

         A7: v1 in (W2 /\ W3) by A5, Th3;

        u1 in (W1 /\ W2) by A4, A6, Th3;

        then x in ((W1 /\ W2) + (W2 /\ W3)) by A3, A7, Th1;

        hence thesis by STRUCT_0:def 5;

      end;

      thus thesis by Lm8;

    end;

    theorem :: RUSUB_2:26

    for V be RealUnitarySpace, W1,W2,W3 be Subspace of V st W1 is Subspace of W2 holds (W2 /\ (W1 + W3)) = ((W1 /\ W2) + (W2 /\ W3)) by Lm9, RUSUB_1: 24;

    

     Lm10: for V be RealUnitarySpace, W1,W2,W3 be Subspace of V holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))

    proof

      let V be RealUnitarySpace;

      let W1,W2,W3 be Subspace of V;

      let x be object;

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

      then x in { (u + v) where u,v be VECTOR of V : u in W2 & v in (W1 /\ W3) } by Def1;

      then

      consider u,v be VECTOR of V such that

       A1: x = (u + v) & u in W2 and

       A2: v in (W1 /\ W3);

      v in W3 by A2, Th3;

      then x in { (u1 + u2) where u1,u2 be VECTOR of V : u1 in W2 & u2 in W3 } by A1;

      then

       A3: x in the carrier of (W2 + W3) by Def1;

      v in W1 by A2, Th3;

      then x in { (v1 + v2) where v1,v2 be VECTOR of V : v1 in W1 & v2 in W2 } by A1;

      then x in the carrier of (W1 + W2) by Def1;

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

      hence thesis by Def2;

    end;

    theorem :: RUSUB_2:27

    for V be RealUnitarySpace, W1,W2,W3 be Subspace of V holds (W2 + (W1 /\ W3)) is Subspace of ((W1 + W2) /\ (W2 + W3)) by Lm10, RUSUB_1: 22;

    

     Lm11: for V be RealUnitarySpace, W1,W2,W3 be Subspace of V st W1 is Subspace of W2 holds the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))

    proof

      let V be RealUnitarySpace;

      let W1,W2,W3 be Subspace of V;

      reconsider V2 = the carrier of W2 as Subset of V by RUSUB_1:def 1;

      

       A1: V2 is linearly-closed by RUSUB_1: 28;

      assume W1 is Subspace of W2;

      then

       A2: the carrier of W1 c= the carrier of W2 by RUSUB_1:def 1;

      thus the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3)) by Lm10;

      let x be object;

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

      then x in (the carrier of (W1 + W2) /\ the carrier of (W2 + W3)) by Def2;

      then x in the carrier of (W1 + W2) by XBOOLE_0:def 4;

      then x in { (u1 + u2) where u1,u2 be VECTOR of V : u1 in W1 & u2 in W2 } by Def1;

      then

      consider u1,u2 be VECTOR of V such that

       A3: x = (u1 + u2) and

       A4: u1 in W1 & u2 in W2;

      u1 in the carrier of W1 & u2 in the carrier of W2 by A4, STRUCT_0:def 5;

      then (u1 + u2) in V2 by A2, A1, RLSUB_1:def 1;

      then

       A5: (u1 + u2) in W2 by STRUCT_0:def 5;

      ( 0. V) in (W1 /\ W3) & ((u1 + u2) + ( 0. V)) = (u1 + u2) by RLVECT_1: 4, RUSUB_1: 11;

      then x in { (u + v) where u,v be VECTOR of V : u in W2 & v in (W1 /\ W3) } by A3, A5;

      hence thesis by Def1;

    end;

    theorem :: RUSUB_2:28

    for V be RealUnitarySpace, W1,W2,W3 be Subspace of V st W1 is Subspace of W2 holds (W2 + (W1 /\ W3)) = ((W1 + W2) /\ (W2 + W3)) by Lm11, RUSUB_1: 24;

    theorem :: RUSUB_2:29

    

     Th29: for V be RealUnitarySpace, W1,W2,W3 be Subspace of V st W1 is strict Subspace of W3 holds (W1 + (W2 /\ W3)) = ((W1 + W2) /\ W3)

    proof

      let V be RealUnitarySpace;

      let W1,W2,W3 be Subspace of V;

      assume

       A1: W1 is strict Subspace of W3;

      

      thus ((W1 + W2) /\ W3) = (W3 /\ (W1 + W2)) by Th14

      .= ((W1 /\ W3) + (W3 /\ W2)) by A1, Lm9, RUSUB_1: 24

      .= (W1 + (W3 /\ W2)) by A1, Th17

      .= (W1 + (W2 /\ W3)) by Th14;

    end;

    theorem :: RUSUB_2:30

    for V be RealUnitarySpace, W1,W2 be strict Subspace of V holds (W1 + W2) = W2 iff (W1 /\ W2) = W1

    proof

      let V be RealUnitarySpace;

      let W1,W2 be strict Subspace of V;

      (W1 + W2) = W2 iff W1 is Subspace of W2 by Th8;

      hence thesis by Th17;

    end;

    theorem :: RUSUB_2:31

    for V be RealUnitarySpace, W1 be Subspace of V, W2,W3 be strict Subspace of V holds W1 is Subspace of W2 implies (W1 + W3) is Subspace of (W2 + W3)

    proof

      let V be RealUnitarySpace;

      let W1 be Subspace of V;

      let W2,W3 be strict Subspace of V;

      assume

       A1: W1 is Subspace of W2;

      ((W1 + W3) + (W2 + W3)) = ((W1 + W3) + (W3 + W2)) by Lm1

      .= (((W1 + W3) + W3) + W2) by Th6

      .= ((W1 + (W3 + W3)) + W2) by Th6

      .= ((W1 + W3) + W2) by Lm3

      .= (W1 + (W3 + W2)) by Th6

      .= (W1 + (W2 + W3)) by Lm1

      .= ((W1 + W2) + W3) by Th6

      .= (W2 + W3) by A1, Th8;

      hence thesis by Th8;

    end;

    theorem :: RUSUB_2:32

    for V be RealUnitarySpace, W1,W2 be Subspace of V holds (ex W be Subspace of V st the carrier of W = (the carrier of W1 \/ the carrier of W2)) iff W1 is Subspace of W2 or W2 is Subspace of W1

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      set VW1 = the carrier of W1;

      set VW2 = the carrier of W2;

      thus (ex W be Subspace of V st the carrier of W = (the carrier of W1 \/ the carrier of W2)) implies W1 is Subspace of W2 or W2 is Subspace of W1

      proof

        given W be Subspace of V such that

         A1: the carrier of W = (the carrier of W1 \/ the carrier of W2);

        set VW = the carrier of W;

        assume that

         A2: not W1 is Subspace of W2 and

         A3: not W2 is Subspace of W1;

         not VW2 c= VW1 by A3, RUSUB_1: 22;

        then

        consider y be object such that

         A4: y in VW2 and

         A5: not y in VW1;

        reconsider y as Element of VW2 by A4;

        reconsider y as VECTOR of V by RUSUB_1: 3;

        reconsider A1 = VW as Subset of V by RUSUB_1:def 1;

        

         A6: A1 is linearly-closed by RUSUB_1: 28;

         not VW1 c= VW2 by A2, RUSUB_1: 22;

        then

        consider x be object such that

         A7: x in VW1 and

         A8: not x in VW2;

        reconsider x as Element of VW1 by A7;

        reconsider x as VECTOR of V by RUSUB_1: 3;

         A9:

        now

          reconsider A2 = VW2 as Subset of V by RUSUB_1:def 1;

          

           A10: A2 is linearly-closed by RUSUB_1: 28;

          assume (x + y) in VW2;

          then ((x + y) - y) in VW2 by A10, RLSUB_1: 3;

          then (x + (y - y)) in VW2 by RLVECT_1:def 3;

          then (x + ( 0. V)) in VW2 by RLVECT_1: 15;

          hence contradiction by A8, RLVECT_1: 4;

        end;

         A11:

        now

          reconsider A2 = VW1 as Subset of V by RUSUB_1:def 1;

          

           A12: A2 is linearly-closed by RUSUB_1: 28;

          assume (x + y) in VW1;

          then ((y + x) - x) in VW1 by A12, RLSUB_1: 3;

          then (y + (x - x)) in VW1 by RLVECT_1:def 3;

          then (y + ( 0. V)) in VW1 by RLVECT_1: 15;

          hence contradiction by A5, RLVECT_1: 4;

        end;

        x in VW & y in VW by A1, XBOOLE_0:def 3;

        then (x + y) in VW by A6, RLSUB_1:def 1;

        hence thesis by A1, A11, A9, XBOOLE_0:def 3;

      end;

       A13:

      now

        assume W1 is Subspace of W2;

        then VW1 c= VW2 by RUSUB_1:def 1;

        then (VW1 \/ VW2) = VW2 by XBOOLE_1: 12;

        hence thesis;

      end;

       A14:

      now

        assume W2 is Subspace of W1;

        then VW2 c= VW1 by RUSUB_1:def 1;

        then (VW1 \/ VW2) = VW1 by XBOOLE_1: 12;

        hence thesis;

      end;

      assume W1 is Subspace of W2 or W2 is Subspace of W1;

      hence thesis by A13, A14;

    end;

    begin

    definition

      let V be RealUnitarySpace;

      :: RUSUB_2:def3

      func Subspaces (V) -> set means

      : Def3: for x be object holds x in it iff x is strict Subspace of V;

      existence

      proof

        defpred P[ object, object] means ex W be strict Subspace of V st $2 = W & $1 = the carrier of W;

        defpred P[ object] means ex W be strict Subspace of V st $1 = the carrier of W;

        consider B be set such that

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

        

         A2: for x,y1,y2 be object st P[x, y1] & P[x, y2] holds y1 = y2 by RUSUB_1: 24;

        consider f be Function such that

         A3: for x,y be object holds [x, y] in f iff x in B & P[x, y] from FUNCT_1:sch 1( A2);

        for x be object holds x in B iff ex y be object st [x, y] in f

        proof

          let x be object;

          thus x in B implies ex y be object st [x, y] in f

          proof

            assume

             A4: x in B;

            then

            consider W be strict Subspace of V such that

             A5: x = the carrier of W by A1;

            take W;

            thus thesis by A3, A4, A5;

          end;

          thus thesis by A3;

        end;

        then

         A6: B = ( dom f) by XTUPLE_0:def 12;

        for y be object holds y in ( rng f) iff y is strict Subspace of V

        proof

          let y be object;

          thus y in ( rng f) implies y is strict Subspace of V

          proof

            assume y in ( rng f);

            then

            consider x be object such that

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

             [x, y] in f by A7, FUNCT_1:def 2;

            then ex W be strict Subspace of V st y = W & x = the carrier of W by A3;

            hence thesis;

          end;

          assume y is strict Subspace of V;

          then

          reconsider W = y as strict Subspace of V;

          reconsider x = the carrier of W as set;

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

          then

           A8: x in ( dom f) by A1, A6;

          

           A9: y is set by TARSKI: 1;

           [x, y] in f by A3, A6, A8;

          then y = (f . x) by A8, FUNCT_1:def 2, A9;

          hence thesis by A8, FUNCT_1:def 3;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let D1,D2 be set;

        assume

         A10: for x be object holds x in D1 iff x is strict Subspace of V;

        assume

         A11: for x be object holds x in D2 iff x is strict Subspace of V;

        now

          let x be object;

          thus x in D1 implies x in D2

          proof

            assume x in D1;

            then x is strict Subspace of V by A10;

            hence thesis by A11;

          end;

          assume x in D2;

          then x is strict Subspace of V by A11;

          hence x in D1 by A10;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    registration

      let V be RealUnitarySpace;

      cluster ( Subspaces V) -> non empty;

      coherence

      proof

        set x = the strict Subspace of V;

        x in ( Subspaces V) by Def3;

        hence thesis;

      end;

    end

    theorem :: RUSUB_2:33

    for V be strict RealUnitarySpace holds V in ( Subspaces V)

    proof

      let V be strict RealUnitarySpace;

      ( (Omega). V) in ( Subspaces V) by Def3;

      hence thesis by RUSUB_1:def 3;

    end;

    begin

    definition

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      :: RUSUB_2:def4

      pred V is_the_direct_sum_of W1,W2 means the UNITSTR of V = (W1 + W2) & (W1 /\ W2) = ( (0). V);

    end

    

     Lm12: for V be RealUnitarySpace, W be strict Subspace of V st (for v be VECTOR of V holds v in W) holds W = the UNITSTR of V

    proof

      let V be RealUnitarySpace, W be strict Subspace of V;

      assume

       A1: for v be VECTOR of V holds v in W;

      now

        let v be VECTOR of V;

        thus v in W implies v in ( (Omega). V)

        proof

          assume v in W;

          v in the UNITSTR of V by RLVECT_1: 1;

          hence thesis by RUSUB_1:def 3;

        end;

        assume v in ( (Omega). V);

        thus v in W by A1;

      end;

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

      hence thesis by RUSUB_1:def 3;

    end;

    

     Lm13: for V be RealUnitarySpace, W1,W2 be Subspace of V holds (W1 + W2) = the UNITSTR of V iff for v be VECTOR of V holds ex v1,v2 be VECTOR of V st v1 in W1 & v2 in W2 & v = (v1 + v2)

    proof

      let V be RealUnitarySpace, W1,W2 be Subspace of V;

      thus (W1 + W2) = the UNITSTR of V implies for v be VECTOR of V holds ex v1,v2 be VECTOR of V st v1 in W1 & v2 in W2 & v = (v1 + v2) by RLVECT_1: 1, Th1;

      assume

       A1: for v be VECTOR of V holds ex v1,v2 be VECTOR of V st v1 in W1 & v2 in W2 & v = (v1 + v2);

      now

        let u be VECTOR of V;

        ex v1,v2 be VECTOR of V st v1 in W1 & v2 in W2 & u = (v1 + v2) by A1;

        hence u in (W1 + W2) by Th1;

      end;

      hence thesis by Lm12;

    end;

    

     Lm14: for V be RealUnitarySpace, W be Subspace of V holds ex C be strict Subspace of V st V is_the_direct_sum_of (C,W)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      defpred P[ object] means ex W1 be strict Subspace of V st $1 = W1 & (W /\ W1) = ( (0). V);

      consider X be set such that

       A1: for x be object holds x in X iff x in ( Subspaces V) & P[x] from XBOOLE_0:sch 1;

      (W /\ ( (0). V)) = ( (0). V) & ( (0). V) in ( Subspaces V) by Def3, Th18;

      then

      reconsider X as non empty set by A1;

      defpred P[ object, object] means ex W1,W2 be strict Subspace of V st $1 = W1 & $2 = W2 & W1 is Subspace of W2;

      consider R be Relation of X such that

       A2: for x,y be Element of X holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

      defpred Q[ set, set] means [$1, $2] in R;

       A3:

      now

        let x,y,z be Element of X;

        assume that

         A4: Q[x, y] and

         A5: Q[y, z];

        consider W1,W2 be strict Subspace of V such that

         A6: x = W1 and

         A7: y = W2 & W1 is Subspace of W2 by A2, A4;

        consider W3,W4 be strict Subspace of V such that

         A8: y = W3 and

         A9: z = W4 and

         A10: W3 is Subspace of W4 by A2, A5;

        W1 is strict Subspace of W4 by A7, A8, A10, RUSUB_1: 21;

        hence Q[x, z] by A2, A6, A9;

      end;

      

       A11: for Y be set st Y c= X & (for x,y be Element of X st x in Y & y in Y holds Q[x, y] or Q[y, x]) holds ex y be Element of X st for x be Element of X st x in Y holds Q[x, y]

      proof

        let Y be set;

        assume that

         A12: Y c= X and

         A13: for x,y be Element of X st x in Y & y in Y holds [x, y] in R or [y, x] in R;

        now

          per cases ;

            suppose

             A14: Y = {} ;

            set y = the Element of X;

            take y9 = y;

            let x be Element of X;

            assume x in Y;

            hence [x, y9] in R by A14;

          end;

            suppose

             A15: Y <> {} ;

            defpred P[ object, object] means ex W1 be strict Subspace of V st $1 = W1 & $2 = the carrier of W1;

            

             A16: for x be object st x in Y holds ex y be object st P[x, y]

            proof

              let x be object;

              assume x in Y;

              then

              consider W1 be strict Subspace of V such that

               A17: x = W1 and (W /\ W1) = ( (0). V) by A1, A12;

              reconsider y = the carrier of W1 as set;

              take y;

              take W1;

              thus thesis by A17;

            end;

            consider f be Function such that

             A18: ( dom f) = Y and

             A19: for x be object st x in Y holds P[x, (f . x)] from CLASSES1:sch 1( A16);

            set Z = ( union ( rng f));

             A20:

            now

              let x be object;

              assume x in Z;

              then

              consider Y9 be set such that

               A21: x in Y9 and

               A22: Y9 in ( rng f) by TARSKI:def 4;

              consider y be object such that

               A23: y in ( dom f) and

               A24: (f . y) = Y9 by A22, FUNCT_1:def 3;

              consider W1 be strict Subspace of V such that y = W1 and

               A25: (f . y) = the carrier of W1 by A18, A19, A23;

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

              hence x in the carrier of V by A21, A24, A25;

            end;

            set z = the Element of ( rng f);

            

             A26: ( rng f) <> {} by A15, A18, RELAT_1: 42;

            then

            consider z1 be object such that

             A27: z1 in ( dom f) and

             A28: (f . z1) = z by FUNCT_1:def 3;

            reconsider Z as Subset of V by A20, TARSKI:def 3;

            ex W3 be strict Subspace of V st z1 = W3 & (f . z1) = the carrier of W3 by A18, A19, A27;

            then

             A29: Z <> {} by A26, A28, ORDERS_1: 6;

            

             A30: for v1,v2 be VECTOR of V st v1 in Z & v2 in Z holds (v1 + v2) in Z

            proof

              let v1,v2 be VECTOR of V;

              assume that

               A31: v1 in Z and

               A32: v2 in Z;

              consider Y1 be set such that

               A33: v1 in Y1 and

               A34: Y1 in ( rng f) by A31, TARSKI:def 4;

              consider y1 be object such that

               A35: y1 in ( dom f) and

               A36: (f . y1) = Y1 by A34, FUNCT_1:def 3;

              consider Y2 be set such that

               A37: v2 in Y2 and

               A38: Y2 in ( rng f) by A32, TARSKI:def 4;

              consider y2 be object such that

               A39: y2 in ( dom f) and

               A40: (f . y2) = Y2 by A38, FUNCT_1:def 3;

              consider W1 be strict Subspace of V such that

               A41: y1 = W1 and

               A42: (f . y1) = the carrier of W1 by A18, A19, A35;

              consider W2 be strict Subspace of V such that

               A43: y2 = W2 and

               A44: (f . y2) = the carrier of W2 by A18, A19, A39;

              reconsider y1, y2 as Element of X by A12, A18, A35, A39;

              now

                per cases by A13, A18, A35, A39;

                  suppose [y1, y2] in R;

                  then ex W3,W4 be strict Subspace of V st y1 = W3 & y2 = W4 & W3 is Subspace of W4 by A2;

                  then the carrier of W1 c= the carrier of W2 by A41, A43, RUSUB_1:def 1;

                  then

                   A45: v1 in W2 by A33, A36, A42, STRUCT_0:def 5;

                  v2 in W2 by A37, A40, A44, STRUCT_0:def 5;

                  then (v1 + v2) in W2 by A45, RUSUB_1: 14;

                  then

                   A46: (v1 + v2) in the carrier of W2 by STRUCT_0:def 5;

                  (f . y2) in ( rng f) by A39, FUNCT_1:def 3;

                  hence thesis by A44, A46, TARSKI:def 4;

                end;

                  suppose [y2, y1] in R;

                  then ex W3,W4 be strict Subspace of V st y2 = W3 & y1 = W4 & W3 is Subspace of W4 by A2;

                  then the carrier of W2 c= the carrier of W1 by A41, A43, RUSUB_1:def 1;

                  then

                   A47: v2 in W1 by A37, A40, A44, STRUCT_0:def 5;

                  v1 in W1 by A33, A36, A42, STRUCT_0:def 5;

                  then (v1 + v2) in W1 by A47, RUSUB_1: 14;

                  then

                   A48: (v1 + v2) in the carrier of W1 by STRUCT_0:def 5;

                  (f . y1) in ( rng f) by A35, FUNCT_1:def 3;

                  hence thesis by A42, A48, TARSKI:def 4;

                end;

              end;

              hence thesis;

            end;

            for a be Real, v1 be VECTOR of V st v1 in Z holds (a * v1) in Z

            proof

              let a be Real;

              let v1 be VECTOR of V;

              assume v1 in Z;

              then

              consider Y1 be set such that

               A49: v1 in Y1 and

               A50: Y1 in ( rng f) by TARSKI:def 4;

              consider y1 be object such that

               A51: y1 in ( dom f) and

               A52: (f . y1) = Y1 by A50, FUNCT_1:def 3;

              consider W1 be strict Subspace of V such that y1 = W1 and

               A53: (f . y1) = the carrier of W1 by A18, A19, A51;

              v1 in W1 by A49, A52, A53, STRUCT_0:def 5;

              then (a * v1) in W1 by RUSUB_1: 15;

              then

               A54: (a * v1) in the carrier of W1 by STRUCT_0:def 5;

              (f . y1) in ( rng f) by A51, FUNCT_1:def 3;

              hence thesis by A53, A54, TARSKI:def 4;

            end;

            then Z is linearly-closed by A30, RLSUB_1:def 1;

            then

            consider E be strict Subspace of V such that

             A55: Z = the carrier of E by A29, RUSUB_1: 29;

            now

              let u be VECTOR of V;

              thus u in (W /\ E) implies u in ( (0). V)

              proof

                assume

                 A56: u in (W /\ E);

                then

                 A57: u in W by Th3;

                u in E by A56, Th3;

                then u in Z by A55, STRUCT_0:def 5;

                then

                consider Y1 be set such that

                 A58: u in Y1 and

                 A59: Y1 in ( rng f) by TARSKI:def 4;

                consider y1 be object such that

                 A60: y1 in ( dom f) and

                 A61: (f . y1) = Y1 by A59, FUNCT_1:def 3;

                

                 A62: ex W2 be strict Subspace of V st y1 = W2 & (W /\ W2) = ( (0). V) by A1, A12, A18, A60;

                consider W1 be strict Subspace of V such that

                 A63: y1 = W1 and

                 A64: (f . y1) = the carrier of W1 by A18, A19, A60;

                u in W1 by A58, A61, A64, STRUCT_0:def 5;

                hence thesis by A63, A57, A62, Th3;

              end;

              assume u in ( (0). V);

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

              then u in {( 0. V)} by RUSUB_1:def 2;

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

              hence u in (W /\ E) by RUSUB_1: 11;

            end;

            then

             A65: (W /\ E) = ( (0). V) by RUSUB_1: 25;

            E in ( Subspaces V) by Def3;

            then

            reconsider y9 = E as Element of X by A1, A65;

            take y = y9;

            let x be Element of X;

            assume

             A66: x in Y;

            then

            consider W1 be strict Subspace of V such that

             A67: x = W1 and

             A68: (f . x) = the carrier of W1 by A19;

            now

              let u be VECTOR of V;

              assume u in W1;

              then

               A69: u in the carrier of W1 by STRUCT_0:def 5;

              the carrier of W1 in ( rng f) by A18, A66, A68, FUNCT_1:def 3;

              then u in Z by A69, TARSKI:def 4;

              hence u in E by A55, STRUCT_0:def 5;

            end;

            then W1 is strict Subspace of E by RUSUB_1: 23;

            hence [x, y] in R by A2, A67;

          end;

        end;

        hence thesis;

      end;

       A70:

      now

        let x be Element of X;

        x in ( Subspaces V) by A1;

        hence x is strict Subspace of V by Def3;

      end;

       A71:

      now

        let x be Element of X;

        reconsider W = x as strict Subspace of V by A70;

        W is Subspace of W by RUSUB_1: 19;

        hence Q[x, x] by A2;

      end;

       A72:

      now

        let x,y be Element of X;

        assume Q[x, y] & Q[y, x];

        then (ex W1,W2 be strict Subspace of V st x = W1 & y = W2 & W1 is Subspace of W2) & ex W3,W4 be strict Subspace of V st y = W3 & x = W4 & W3 is Subspace of W4 by A2;

        hence x = y by RUSUB_1: 20;

      end;

      consider x be Element of X such that

       A73: for y be Element of X st x <> y holds not Q[x, y] from ORDERS_1:sch 1( A71, A72, A3, A11);

      consider L be strict Subspace of V such that

       A74: x = L and

       A75: (W /\ L) = ( (0). V) by A1;

      take L;

      thus the UNITSTR of V = (L + W)

      proof

        assume not thesis;

        then

        consider v be VECTOR of V such that

         A76: for v1,v2 be VECTOR of V holds not v1 in L or not v2 in W or v <> (v1 + v2) by Lm13;

        v = (( 0. V) + v) & ( 0. V) in W by RLVECT_1: 4, RUSUB_1: 11;

        then

         A77: not v in L by A76;

        set A = the set of all (a * v) where a be Real;

        

         A78: (1 * v) in A;

        now

          let x be object;

          assume x in A;

          then ex a be Real st x = (a * v);

          hence x in the carrier of V;

        end;

        then

        reconsider A as Subset of V by TARSKI:def 3;

        

         A79: for v1,v2 be VECTOR of V st v1 in A & v2 in A holds (v1 + v2) in A

        proof

          let v1,v2 be VECTOR of V;

          assume v1 in A;

          then

          consider a1 be Real such that

           A80: v1 = (a1 * v);

          assume v2 in A;

          then

          consider a2 be Real such that

           A81: v2 = (a2 * v);

          (v1 + v2) = ((a1 + a2) * v) by A80, A81, RLVECT_1:def 6;

          hence thesis;

        end;

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

        proof

          let a be Real;

          let v1 be VECTOR of V;

          assume v1 in A;

          then

          consider a1 be Real such that

           A82: v1 = (a1 * v);

          (a * v1) = ((a * a1) * v) by A82, RLVECT_1:def 7;

          hence thesis;

        end;

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

        then

        consider Z be strict Subspace of V such that

         A83: the carrier of Z = A by A78, RUSUB_1: 29;

        

         A84: not v in (L + W) by A76, Th1;

        now

          let u be VECTOR of V;

          thus u in (Z /\ (W + L)) implies u in ( (0). V)

          proof

            assume

             A85: u in (Z /\ (W + L));

            then u in Z by Th3;

            then u in A by A83, STRUCT_0:def 5;

            then

            consider a be Real such that

             A86: u = (a * v);

            now

              reconsider aa = a as Real;

              u in (W + L) by A85, Th3;

              then ((aa " ) * (aa * v)) in (W + L) by A86, RUSUB_1: 15;

              then

               A87: (((a " ) * a) * v) in (W + L) by RLVECT_1:def 7;

              assume a <> 0 ;

              then (1 * v) in (W + L) by A87, XCMPLX_0:def 7;

              then (1 * v) in (L + W) by Lm1;

              hence contradiction by A84, RLVECT_1:def 8;

            end;

            then u = ( 0. V) by A86, RLVECT_1: 10;

            hence thesis by RUSUB_1: 11;

          end;

          assume u in ( (0). V);

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

          then u in {( 0. V)} by RUSUB_1:def 2;

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

          hence u in (Z /\ (W + L)) by RUSUB_1: 11;

        end;

        then

         A88: (Z /\ (W + L)) = ( (0). V) by RUSUB_1: 25;

        now

          let u be VECTOR of V;

          thus u in ((Z + L) /\ W) implies u in ( (0). V)

          proof

            assume

             A89: u in ((Z + L) /\ W);

            then u in (Z + L) by Th3;

            then

            consider v1,v2 be VECTOR of V such that

             A90: v1 in Z and

             A91: v2 in L and

             A92: u = (v1 + v2) by Th1;

            

             A93: u in W by A89, Th3;

            then

             A94: u in (W + L) by Th2;

            v1 = (u - v2) & v2 in (W + L) by A91, A92, Th2, RLSUB_2: 61;

            then v1 in (W + L) by A94, RUSUB_1: 17;

            then v1 in (Z /\ (W + L)) by A90, Th3;

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

            then v1 in {( 0. V)} by RUSUB_1:def 2;

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

            then v2 = u by A92, RLVECT_1: 4;

            hence thesis by A75, A91, A93, Th3;

          end;

          assume u in ( (0). V);

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

          then u in {( 0. V)} by RUSUB_1:def 2;

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

          hence u in ((Z + L) /\ W) by RUSUB_1: 11;

        end;

        then ((Z + L) /\ W) = ( (0). V) by RUSUB_1: 25;

        then

         A95: (W /\ (Z + L)) = ( (0). V) by Th14;

        (Z + L) in ( Subspaces V) by Def3;

        then

        reconsider x1 = (Z + L) as Element of X by A1, A95;

        L is Subspace of (Z + L) by Th7;

        then

         A96: [x, x1] in R by A2, A74;

        v in A by A78, RLVECT_1:def 8;

        then v in Z by A83, STRUCT_0:def 5;

        then (Z + L) <> L by A77, Th2;

        hence contradiction by A73, A74, A96;

      end;

      thus thesis by A75, Th14;

    end;

    definition

      let V be RealUnitarySpace;

      let W be Subspace of V;

      :: RUSUB_2:def5

      mode Linear_Compl of W -> Subspace of V means

      : Def5: V is_the_direct_sum_of (it ,W);

      existence

      proof

        ex C be strict Subspace of V st V is_the_direct_sum_of (C,W) by Lm14;

        hence thesis;

      end;

    end

    registration

      let V be RealUnitarySpace;

      let W be Subspace of V;

      cluster strict for Linear_Compl of W;

      existence

      proof

        consider C be strict Subspace of V such that

         A1: V is_the_direct_sum_of (C,W) by Lm14;

        C is Linear_Compl of W by A1, Def5;

        hence thesis;

      end;

    end

    

     Lm15: for V be RealUnitarySpace, W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds V is_the_direct_sum_of (W2,W1) by Th14, Lm1;

    theorem :: RUSUB_2:34

    for V be RealUnitarySpace, W1,W2 be Subspace of V holds V is_the_direct_sum_of (W1,W2) implies W2 is Linear_Compl of W1 by Lm15, Def5;

    theorem :: RUSUB_2:35

    

     Th35: for V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W holds V is_the_direct_sum_of (L,W) & V is_the_direct_sum_of (W,L) by Def5, Lm15;

    begin

    theorem :: RUSUB_2:36

    

     Th36: for V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W holds (W + L) = the UNITSTR of V & (L + W) = the UNITSTR of V

    proof

      let V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W;

      V is_the_direct_sum_of (W,L) by Th35;

      hence (W + L) = the UNITSTR of V;

      hence thesis by Lm1;

    end;

    theorem :: RUSUB_2:37

    

     Th37: for V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W holds (W /\ L) = ( (0). V) & (L /\ W) = ( (0). V)

    proof

      let V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W;

      V is_the_direct_sum_of (W,L) by Th35;

      hence (W /\ L) = ( (0). V);

      hence thesis by Th14;

    end;

    theorem :: RUSUB_2:38

    for V be RealUnitarySpace, W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds V is_the_direct_sum_of (W2,W1) by Lm15;

    theorem :: RUSUB_2:39

    

     Th39: for V be RealUnitarySpace holds V is_the_direct_sum_of (( (0). V),( (Omega). V)) & V is_the_direct_sum_of (( (Omega). V),( (0). V)) by Th10, Th18;

    theorem :: RUSUB_2:40

    for V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W holds W is Linear_Compl of L

    proof

      let V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W;

      V is_the_direct_sum_of (L,W) by Def5;

      then V is_the_direct_sum_of (W,L) by Lm15;

      hence thesis by Def5;

    end;

    theorem :: RUSUB_2:41

    for V be RealUnitarySpace holds ( (0). V) is Linear_Compl of ( (Omega). V) & ( (Omega). V) is Linear_Compl of ( (0). V) by Th39, Def5;

    

     Lm16: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V, x be set holds x in (v + W) iff ex u be VECTOR of V st u in W & x = (v + u)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      let x be set;

      thus x in (v + W) implies ex u be VECTOR of V st u in W & x = (v + u)

      proof

        assume x in (v + W);

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

        then

        consider u be VECTOR of V such that

         A1: x = (v + u) & u in W;

        take u;

        thus thesis by A1;

      end;

      given u be VECTOR of V such that

       A2: u in W & x = (v + u);

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

      hence thesis by RUSUB_1:def 4;

    end;

    theorem :: RUSUB_2:42

    

     Th42: for V be RealUnitarySpace, W1,W2 be Subspace of V, C1 be Coset of W1, C2 be Coset of W2 st C1 meets C2 holds (C1 /\ C2) is Coset of (W1 /\ W2)

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      let C1 be Coset of W1;

      let C2 be Coset of W2;

      set v = the Element of (C1 /\ C2);

      set C = (C1 /\ C2);

      assume

       A1: (C1 /\ C2) <> {} ;

      then

      reconsider v as Element of V by TARSKI:def 3;

      v in C1 by A1, XBOOLE_0:def 4;

      then

       A2: C1 = (v + W1) by RUSUB_1: 72;

      v in C2 by A1, XBOOLE_0:def 4;

      then

       A3: C2 = (v + W2) by RUSUB_1: 72;

      reconsider v as VECTOR of V;

      

       A4: (v + (W1 /\ W2)) c= C

      proof

        let x be object;

        assume x in (v + (W1 /\ W2));

        then

        consider u be VECTOR of V such that

         A5: u in (W1 /\ W2) and

         A6: x = (v + u) by Lm16;

        u in W2 by A5, Th3;

        then x in { (v + u2) where u2 be VECTOR of V : u2 in W2 } by A6;

        then

         A7: x in C2 by A3, RUSUB_1:def 4;

        u in W1 by A5, Th3;

        then x in { (v + u1) where u1 be VECTOR of V : u1 in W1 } by A6;

        then x in C1 by A2, RUSUB_1:def 4;

        hence thesis by A7, XBOOLE_0:def 4;

      end;

      C c= (v + (W1 /\ W2))

      proof

        let x be object;

        assume

         A8: x in C;

        then x in C1 by XBOOLE_0:def 4;

        then

        consider u1 be VECTOR of V such that

         A9: u1 in W1 and

         A10: x = (v + u1) by A2, Lm16;

        x in C2 by A8, XBOOLE_0:def 4;

        then

        consider u2 be VECTOR of V such that

         A11: u2 in W2 and

         A12: x = (v + u2) by A3, Lm16;

        u1 = u2 by A10, A12, RLVECT_1: 8;

        then u1 in (W1 /\ W2) by A9, A11, Th3;

        then x in { (v + u) where u be VECTOR of V : u in (W1 /\ W2) } by A10;

        hence thesis by RUSUB_1:def 4;

      end;

      then C = (v + (W1 /\ W2)) by A4;

      hence thesis by RUSUB_1:def 5;

    end;

    

     Lm17: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V holds ex C be Coset of W st v in C

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      reconsider C = (v + W) as Coset of W by RUSUB_1:def 5;

      take C;

      thus thesis by RUSUB_1: 37;

    end;

    theorem :: RUSUB_2:43

    

     Th43: for V be RealUnitarySpace, W1,W2 be Subspace of V holds V is_the_direct_sum_of (W1,W2) iff for C1 be Coset of W1, C2 be Coset of W2 holds ex v be VECTOR of V st (C1 /\ C2) = {v}

    proof

      let V be RealUnitarySpace, W1,W2 be Subspace of V;

      set VW1 = the carrier of W1;

      set VW2 = the carrier of W2;

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

      then

       A1: ( 0. V) in VW2 by STRUCT_0:def 5;

      thus V is_the_direct_sum_of (W1,W2) implies for C1 be Coset of W1, C2 be Coset of W2 holds ex v be VECTOR of V st (C1 /\ C2) = {v}

      proof

        assume

         A2: V is_the_direct_sum_of (W1,W2);

        then

         A3: the UNITSTR of V = (W1 + W2);

        let C1 be Coset of W1, C2 be Coset of W2;

        consider v1 be VECTOR of V such that

         A4: C1 = (v1 + W1) by RUSUB_1:def 5;

        v1 in the UNITSTR of V by RLVECT_1: 1;

        then

        consider v11,v12 be VECTOR of V such that

         A5: v11 in W1 and

         A6: v12 in W2 and

         A7: v1 = (v11 + v12) by A3, Th1;

        consider v2 be VECTOR of V such that

         A8: C2 = (v2 + W2) by RUSUB_1:def 5;

        v2 in the UNITSTR of V by RLVECT_1: 1;

        then

        consider v21,v22 be VECTOR of V such that

         A9: v21 in W1 and

         A10: v22 in W2 and

         A11: v2 = (v21 + v22) by A3, Th1;

        take v = (v12 + v21);

         {v} = (C1 /\ C2)

        proof

          thus

           A12: {v} c= (C1 /\ C2)

          proof

            let x be object;

            assume x in {v};

            then

             A13: x = v by TARSKI:def 1;

            v21 = (v2 - v22) by A11, RLSUB_2: 61;

            then v21 in C2 by A8, A10, RUSUB_1: 58;

            then C2 = (v21 + W2) by RUSUB_1: 72;

            then

             A14: x in C2 by A6, A13, RUSUB_1: 57;

            v12 = (v1 - v11) by A7, RLSUB_2: 61;

            then v12 in C1 by A4, A5, RUSUB_1: 58;

            then C1 = (v12 + W1) by RUSUB_1: 72;

            then x in C1 by A9, A13, RUSUB_1: 57;

            hence thesis by A14, XBOOLE_0:def 4;

          end;

          let x be object;

          assume

           A15: x in (C1 /\ C2);

          then C1 meets C2;

          then

          reconsider C = (C1 /\ C2) as Coset of (W1 /\ W2) by Th42;

          

           A16: v in {v} by TARSKI:def 1;

          (W1 /\ W2) = ( (0). V) by A2;

          then ex u be VECTOR of V st C = {u} by RUSUB_1: 67;

          hence thesis by A12, A15, A16, TARSKI:def 1;

        end;

        hence thesis;

      end;

      assume

       A17: for C1 be Coset of W1, C2 be Coset of W2 holds ex v be VECTOR of V st (C1 /\ C2) = {v};

      

       A18: VW2 is Coset of W2 by RUSUB_1: 68;

      now

        let u be VECTOR of V;

        consider C1 be Coset of W1 such that

         A19: u in C1 by Lm17;

        consider v be VECTOR of V such that

         A20: (C1 /\ VW2) = {v} by A18, A17;

        

         A21: v in {v} by TARSKI:def 1;

        then v in C1 by A20, XBOOLE_0:def 4;

        then

        consider v1 be VECTOR of V such that

         A22: v1 in W1 and

         A23: (u - v1) = v by A19, RUSUB_1: 74;

        v in VW2 by A20, A21, XBOOLE_0:def 4;

        then

         A24: v in W2 by STRUCT_0:def 5;

        u = (v1 + v) by A23, RLSUB_2: 61;

        hence u in (W1 + W2) by A24, A22, Th1;

      end;

      hence the UNITSTR of V = (W1 + W2) by Lm12;

      VW1 is Coset of W1 by RUSUB_1: 68;

      then

      consider v be VECTOR of V such that

       A25: (VW1 /\ VW2) = {v} by A18, A17;

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

      then ( 0. V) in VW1 by STRUCT_0:def 5;

      then

       A26: ( 0. V) in {v} by A25, A1, XBOOLE_0:def 4;

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

      .= (VW1 /\ VW2) by A25, A26, TARSKI:def 1

      .= the carrier of (W1 /\ W2) by Def2;

      hence thesis by RUSUB_1: 24;

    end;

    begin

    theorem :: RUSUB_2:44

    for V be RealUnitarySpace, W1,W2 be Subspace of V holds (W1 + W2) = the UNITSTR of V iff for v be VECTOR of V holds ex v1,v2 be VECTOR of V st v1 in W1 & v2 in W2 & v = (v1 + v2) by Lm13;

    theorem :: RUSUB_2:45

    

     Th45: for V be RealUnitarySpace, W1,W2 be Subspace of V, v,v1,v2,u1,u2 be VECTOR of V st V is_the_direct_sum_of (W1,W2) & v = (v1 + v2) & v = (u1 + u2) & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds v1 = u1 & v2 = u2

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      let v,v1,v2,u1,u2 be VECTOR of V;

      reconsider C2 = (v1 + W2) as Coset of W2 by RUSUB_1:def 5;

      reconsider C1 = the carrier of W1 as Coset of W1 by RUSUB_1: 68;

      

       A1: v1 in C2 by RUSUB_1: 37;

      assume V is_the_direct_sum_of (W1,W2);

      then

      consider u be VECTOR of V such that

       A2: (C1 /\ C2) = {u} by Th43;

      assume that

       A3: v = (v1 + v2) & v = (u1 + u2) and

       A4: v1 in W1 and

       A5: u1 in W1 and

       A6: v2 in W2 & u2 in W2;

      

       A7: (v2 - u2) in W2 by A6, RUSUB_1: 17;

      v1 in C1 by A4, STRUCT_0:def 5;

      then v1 in (C1 /\ C2) by A1, XBOOLE_0:def 4;

      then

       A8: v1 = u by A2, TARSKI:def 1;

      

       A9: u1 in C1 by A5, STRUCT_0:def 5;

      u1 = ((v1 + v2) - u2) by A3, RLSUB_2: 61

      .= (v1 + (v2 - u2)) by RLVECT_1:def 3;

      then u1 in C2 by A7, Lm16;

      then

       A10: u1 in (C1 /\ C2) by A9, XBOOLE_0:def 4;

      hence v1 = u1 by A2, A8, TARSKI:def 1;

      u1 = u by A10, A2, TARSKI:def 1;

      hence thesis by A3, A8, RLVECT_1: 8;

    end;

    theorem :: RUSUB_2:46

    for V be RealUnitarySpace, W1,W2 be Subspace of V st V = (W1 + W2) & (ex v be VECTOR of V st for v1,v2,u1,u2 be VECTOR of V st v = (v1 + v2) & v = (u1 + u2) & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds v1 = u1 & v2 = u2) holds V is_the_direct_sum_of (W1,W2)

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      assume

       A1: V = (W1 + W2);

      the carrier of ( (0). V) = {( 0. V)} & ( (0). V) is Subspace of (W1 /\ W2) by RUSUB_1: 33, RUSUB_1:def 2;

      then

       A2: {( 0. V)} c= the carrier of (W1 /\ W2) by RUSUB_1:def 1;

      given v be VECTOR of V such that

       A3: for v1,v2,u1,u2 be VECTOR of V st v = (v1 + v2) & v = (u1 + u2) & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds v1 = u1 & v2 = u2;

      assume not thesis;

      then (W1 /\ W2) <> ( (0). V) by A1;

      then the carrier of (W1 /\ W2) <> {( 0. V)} by RUSUB_1:def 2;

      then {( 0. V)} c< the carrier of (W1 /\ W2) by A2;

      then

      consider x be object such that

       A4: x in the carrier of (W1 /\ W2) and

       A5: not x in {( 0. V)} by XBOOLE_0: 6;

      

       A6: x <> ( 0. V) by A5, TARSKI:def 1;

      

       A7: x in (W1 /\ W2) by A4, STRUCT_0:def 5;

      then x in V by RUSUB_1: 2;

      then

      reconsider u = x as VECTOR of V by STRUCT_0:def 5;

      consider v1,v2 be VECTOR of V such that

       A8: v1 in W1 and

       A9: v2 in W2 and

       A10: v = (v1 + v2) by A1, Lm13;

      

       A11: v = ((v1 + v2) + ( 0. V)) by A10, RLVECT_1: 4

      .= ((v1 + v2) + (u - u)) by RLVECT_1: 15

      .= (((v1 + v2) + u) - u) by RLVECT_1:def 3

      .= (((v1 + u) + v2) - u) by RLVECT_1:def 3

      .= ((v1 + u) + (v2 - u)) by RLVECT_1:def 3;

      x in W2 by A7, Th3;

      then

       A12: (v2 - u) in W2 by A9, RUSUB_1: 17;

      x in W1 by A7, Th3;

      then (v1 + u) in W1 by A8, RUSUB_1: 14;

      

      then (v2 - u) = v2 by A3, A8, A9, A10, A11, A12

      .= (v2 - ( 0. V)) by RLVECT_1: 13;

      hence thesis by A6, RLVECT_1: 23;

    end;

    definition

      let V be RealUnitarySpace;

      let v be VECTOR of V;

      let W1,W2 be Subspace of V;

      assume

       A1: V is_the_direct_sum_of (W1,W2);

      :: RUSUB_2:def6

      func v |-- (W1,W2) -> Element of [:the carrier of V, the carrier of V:] means

      : Def6: v = ((it `1 ) + (it `2 )) & (it `1 ) in W1 & (it `2 ) in W2;

      existence

      proof

        (W1 + W2) = the UNITSTR of V by A1;

        then

        consider v1,v2 be VECTOR of V such that

         A2: v1 in W1 & v2 in W2 & v = (v1 + v2) by Lm13;

        take [v1, v2];

        thus thesis by A2;

      end;

      uniqueness

      proof

        let t1,t2 be Element of [:the carrier of V, the carrier of V:];

        assume v = ((t1 `1 ) + (t1 `2 )) & (t1 `1 ) in W1 & (t1 `2 ) in W2 & v = ((t2 `1 ) + (t2 `2 )) & (t2 `1 ) in W1 & (t2 `2 ) in W2;

        then

         A3: (t1 `1 ) = (t2 `1 ) & (t1 `2 ) = (t2 `2 ) by A1, Th45;

        t1 = [(t1 `1 ), (t1 `2 )] by MCART_1: 21;

        hence thesis by A3, MCART_1: 21;

      end;

    end

    theorem :: RUSUB_2:47

    

     Th47: for V be RealUnitarySpace, v be VECTOR of V, W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds ((v |-- (W1,W2)) `1 ) = ((v |-- (W2,W1)) `2 )

    proof

      let V be RealUnitarySpace;

      let v be VECTOR of V;

      let W1,W2 be Subspace of V;

      assume

       A1: V is_the_direct_sum_of (W1,W2);

      then

       A2: ((v |-- (W1,W2)) `2 ) in W2 by Def6;

      

       A3: V is_the_direct_sum_of (W2,W1) by A1, Lm15;

      then

       A4: v = (((v |-- (W2,W1)) `2 ) + ((v |-- (W2,W1)) `1 )) & ((v |-- (W2,W1)) `1 ) in W2 by Def6;

      

       A5: ((v |-- (W2,W1)) `2 ) in W1 by A3, Def6;

      v = (((v |-- (W1,W2)) `1 ) + ((v |-- (W1,W2)) `2 )) & ((v |-- (W1,W2)) `1 ) in W1 by A1, Def6;

      hence thesis by A1, A2, A4, A5, Th45;

    end;

    theorem :: RUSUB_2:48

    

     Th48: for V be RealUnitarySpace, v be VECTOR of V, W1,W2 be Subspace of V st V is_the_direct_sum_of (W1,W2) holds ((v |-- (W1,W2)) `2 ) = ((v |-- (W2,W1)) `1 )

    proof

      let V be RealUnitarySpace;

      let v be VECTOR of V;

      let W1,W2 be Subspace of V;

      assume

       A1: V is_the_direct_sum_of (W1,W2);

      then

       A2: ((v |-- (W1,W2)) `2 ) in W2 by Def6;

      

       A3: V is_the_direct_sum_of (W2,W1) by A1, Lm15;

      then

       A4: v = (((v |-- (W2,W1)) `2 ) + ((v |-- (W2,W1)) `1 )) & ((v |-- (W2,W1)) `1 ) in W2 by Def6;

      

       A5: ((v |-- (W2,W1)) `2 ) in W1 by A3, Def6;

      v = (((v |-- (W1,W2)) `1 ) + ((v |-- (W1,W2)) `2 )) & ((v |-- (W1,W2)) `1 ) in W1 by A1, Def6;

      hence thesis by A1, A2, A4, A5, Th45;

    end;

    theorem :: RUSUB_2:49

    for V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W, v be VECTOR of V, t be Element of [:the carrier of V, the carrier of V:] st ((t `1 ) + (t `2 )) = v & (t `1 ) in W & (t `2 ) in L holds t = (v |-- (W,L))

    proof

      let V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W;

      V is_the_direct_sum_of (W,L) by Th35;

      hence thesis by Def6;

    end;

    theorem :: RUSUB_2:50

    for V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W, v be VECTOR of V holds (((v |-- (W,L)) `1 ) + ((v |-- (W,L)) `2 )) = v

    proof

      let V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W;

      V is_the_direct_sum_of (W,L) by Th35;

      hence thesis by Def6;

    end;

    theorem :: RUSUB_2:51

    for V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W, v be VECTOR of V holds ((v |-- (W,L)) `1 ) in W & ((v |-- (W,L)) `2 ) in L

    proof

      let V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W;

      V is_the_direct_sum_of (W,L) by Th35;

      hence thesis by Def6;

    end;

    theorem :: RUSUB_2:52

    for V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W, v be VECTOR of V holds ((v |-- (W,L)) `1 ) = ((v |-- (L,W)) `2 ) by Th35, Th47;

    theorem :: RUSUB_2:53

    for V be RealUnitarySpace, W be Subspace of V, L be Linear_Compl of W, v be VECTOR of V holds ((v |-- (W,L)) `2 ) = ((v |-- (L,W)) `1 ) by Th35, Th48;

    begin

    definition

      let V be RealUnitarySpace;

      :: RUSUB_2:def7

      func SubJoin (V) -> BinOp of ( Subspaces V) means

      : Def7: for A1,A2 be Element of ( Subspaces V), W1,W2 be Subspace of V st A1 = W1 & A2 = W2 holds (it . (A1,A2)) = (W1 + W2);

      existence

      proof

        defpred P[ Element of ( Subspaces V), Element of ( Subspaces V), Element of ( Subspaces V)] means for W1,W2 be Subspace of V st $1 = W1 & $2 = W2 holds $3 = (W1 + W2);

        

         A1: for A1,A2 be Element of ( Subspaces V) holds ex B be Element of ( Subspaces V) st P[A1, A2, B]

        proof

          let A1,A2 be Element of ( Subspaces V);

          reconsider W1 = A1, W2 = A2 as Subspace of V by Def3;

          reconsider C = (W1 + W2) as Element of ( Subspaces V) by Def3;

          take C;

          thus thesis;

        end;

        ex o be BinOp of ( Subspaces V) st for a,b be Element of ( Subspaces V) holds P[a, b, (o . (a,b))] from BINOP_1:sch 3( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of ( Subspaces V);

        assume

         A2: for A1,A2 be Element of ( Subspaces V), W1,W2 be Subspace of V st A1 = W1 & A2 = W2 holds (o1 . (A1,A2)) = (W1 + W2);

        assume

         A3: for A1,A2 be Element of ( Subspaces V), W1,W2 be Subspace of V st A1 = W1 & A2 = W2 holds (o2 . (A1,A2)) = (W1 + W2);

        now

          let x,y be set;

          assume

           A4: x in ( Subspaces V) & y in ( Subspaces V);

          then

          reconsider A = x, B = y as Element of ( Subspaces V);

          reconsider W1 = x, W2 = y as Subspace of V by A4, Def3;

          (o1 . (A,B)) = (W1 + W2) by A2;

          hence (o1 . (x,y)) = (o2 . (x,y)) by A3;

        end;

        hence thesis by BINOP_1: 1;

      end;

    end

    definition

      let V be RealUnitarySpace;

      :: RUSUB_2:def8

      func SubMeet (V) -> BinOp of ( Subspaces V) means

      : Def8: for A1,A2 be Element of ( Subspaces V), W1,W2 be Subspace of V st A1 = W1 & A2 = W2 holds (it . (A1,A2)) = (W1 /\ W2);

      existence

      proof

        defpred P[ Element of ( Subspaces V), Element of ( Subspaces V), Element of ( Subspaces V)] means for W1,W2 be Subspace of V st $1 = W1 & $2 = W2 holds $3 = (W1 /\ W2);

        

         A1: for A1,A2 be Element of ( Subspaces V) holds ex B be Element of ( Subspaces V) st P[A1, A2, B]

        proof

          let A1,A2 be Element of ( Subspaces V);

          reconsider W1 = A1, W2 = A2 as Subspace of V by Def3;

          reconsider C = (W1 /\ W2) as Element of ( Subspaces V) by Def3;

          take C;

          thus thesis;

        end;

        ex o be BinOp of ( Subspaces V) st for a,b be Element of ( Subspaces V) holds P[a, b, (o . (a,b))] from BINOP_1:sch 3( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of ( Subspaces V);

        assume

         A2: for A1,A2 be Element of ( Subspaces V), W1,W2 be Subspace of V st A1 = W1 & A2 = W2 holds (o1 . (A1,A2)) = (W1 /\ W2);

        assume

         A3: for A1,A2 be Element of ( Subspaces V), W1,W2 be Subspace of V st A1 = W1 & A2 = W2 holds (o2 . (A1,A2)) = (W1 /\ W2);

        now

          let x,y be set;

          assume

           A4: x in ( Subspaces V) & y in ( Subspaces V);

          then

          reconsider A = x, B = y as Element of ( Subspaces V);

          reconsider W1 = x, W2 = y as Subspace of V by A4, Def3;

          (o1 . (A,B)) = (W1 /\ W2) by A2;

          hence (o1 . (x,y)) = (o2 . (x,y)) by A3;

        end;

        hence thesis by BINOP_1: 1;

      end;

    end

    begin

    theorem :: RUSUB_2:54

    

     Th54: for V be RealUnitarySpace holds LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #) is Lattice

    proof

      let V be RealUnitarySpace;

      set S = LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #);

      

       A1: for A,B be Element of S holds (A "/\" B) = (B "/\" A)

      proof

        let A,B be Element of S;

        reconsider W1 = A, W2 = B as Subspace of V by Def3;

        

        thus (A "/\" B) = (( SubMeet V) . (A,B)) by LATTICES:def 2

        .= (W1 /\ W2) by Def8

        .= (W2 /\ W1) by Th14

        .= (( SubMeet V) . (B,A)) by Def8

        .= (B "/\" A) by LATTICES:def 2;

      end;

      

       A2: for A,B be Element of S holds ((A "/\" B) "\/" B) = B

      proof

        let A,B be Element of S;

        reconsider W1 = A, W2 = B as strict Subspace of V by Def3;

        reconsider AB = (W1 /\ W2) as Element of S by Def3;

        

        thus ((A "/\" B) "\/" B) = (( SubJoin V) . ((A "/\" B),B)) by LATTICES:def 1

        .= (( SubJoin V) . ((( SubMeet V) . (A,B)),B)) by LATTICES:def 2

        .= (( SubJoin V) . (AB,B)) by Def8

        .= ((W1 /\ W2) + W2) by Def7

        .= B by Lm6, RUSUB_1: 24;

      end;

      

       A3: for A,B,C be Element of S holds (A "\/" (B "\/" C)) = ((A "\/" B) "\/" C)

      proof

        let A,B,C be Element of S;

        reconsider W1 = A, W2 = B, W3 = C as Subspace of V by Def3;

        reconsider AB = (W1 + W2), BC = (W2 + W3) as Element of S by Def3;

        

        thus (A "\/" (B "\/" C)) = (( SubJoin V) . (A,(B "\/" C))) by LATTICES:def 1

        .= (( SubJoin V) . (A,(( SubJoin V) . (B,C)))) by LATTICES:def 1

        .= (( SubJoin V) . (A,BC)) by Def7

        .= (W1 + (W2 + W3)) by Def7

        .= ((W1 + W2) + W3) by Th6

        .= (( SubJoin V) . (AB,C)) by Def7

        .= (( SubJoin V) . ((( SubJoin V) . (A,B)),C)) by Def7

        .= (( SubJoin V) . ((A "\/" B),C)) by LATTICES:def 1

        .= ((A "\/" B) "\/" C) by LATTICES:def 1;

      end;

      

       A4: for A,B be Element of S holds (A "/\" (A "\/" B)) = A

      proof

        let A,B be Element of S;

        reconsider W1 = A, W2 = B as strict Subspace of V by Def3;

        reconsider AB = (W1 + W2) as Element of S by Def3;

        

        thus (A "/\" (A "\/" B)) = (( SubMeet V) . (A,(A "\/" B))) by LATTICES:def 2

        .= (( SubMeet V) . (A,(( SubJoin V) . (A,B)))) by LATTICES:def 1

        .= (( SubMeet V) . (A,AB)) by Def7

        .= (W1 /\ (W1 + W2)) by Def8

        .= A by Lm7, RUSUB_1: 24;

      end;

      

       A5: for A,B,C be Element of S holds (A "/\" (B "/\" C)) = ((A "/\" B) "/\" C)

      proof

        let A,B,C be Element of S;

        reconsider W1 = A, W2 = B, W3 = C as Subspace of V by Def3;

        reconsider AB = (W1 /\ W2), BC = (W2 /\ W3) as Element of S by Def3;

        

        thus (A "/\" (B "/\" C)) = (( SubMeet V) . (A,(B "/\" C))) by LATTICES:def 2

        .= (( SubMeet V) . (A,(( SubMeet V) . (B,C)))) by LATTICES:def 2

        .= (( SubMeet V) . (A,BC)) by Def8

        .= (W1 /\ (W2 /\ W3)) by Def8

        .= ((W1 /\ W2) /\ W3) by Th15

        .= (( SubMeet V) . (AB,C)) by Def8

        .= (( SubMeet V) . ((( SubMeet V) . (A,B)),C)) by Def8

        .= (( SubMeet V) . ((A "/\" B),C)) by LATTICES:def 2

        .= ((A "/\" B) "/\" C) by LATTICES:def 2;

      end;

      for A,B be Element of S holds (A "\/" B) = (B "\/" A)

      proof

        let A,B be Element of S;

        reconsider W1 = A, W2 = B as Subspace of V by Def3;

        

        thus (A "\/" B) = (( SubJoin V) . (A,B)) by LATTICES:def 1

        .= (W1 + W2) by Def7

        .= (W2 + W1) by Lm1

        .= (( SubJoin V) . (B,A)) by Def7

        .= (B "\/" A) by LATTICES:def 1;

      end;

      then S is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A3, A2, A1, A5, A4, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;

      hence thesis;

    end;

    registration

      let V be RealUnitarySpace;

      cluster LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #) -> Lattice-like;

      coherence by Th54;

    end

    theorem :: RUSUB_2:55

    

     Th55: for V be RealUnitarySpace holds LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #) is lower-bounded

    proof

      let V be RealUnitarySpace;

      set S = LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #);

      ex C be Element of S st for A be Element of S holds (C "/\" A) = C & (A "/\" C) = C

      proof

        reconsider C = ( (0). V) as Element of S by Def3;

        take C;

        let A be Element of S;

        reconsider W = A as Subspace of V by Def3;

        

        thus (C "/\" A) = (( SubMeet V) . (C,A)) by LATTICES:def 2

        .= (( (0). V) /\ W) by Def8

        .= C by Th18;

        hence thesis;

      end;

      hence thesis by LATTICES:def 13;

    end;

    theorem :: RUSUB_2:56

    

     Th56: for V be RealUnitarySpace holds LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #) is upper-bounded

    proof

      let V be RealUnitarySpace;

      set S = LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #);

      ex C be Element of S st for A be Element of S holds (C "\/" A) = C & (A "\/" C) = C

      proof

        reconsider C = ( (Omega). V) as Element of S by Def3;

        take C;

        let A be Element of S;

        reconsider W = A as Subspace of V by Def3;

        

        thus (C "\/" A) = (( SubJoin V) . (C,A)) by LATTICES:def 1

        .= (( (Omega). V) + W) by Def7

        .= the UNITSTR of V by Th11

        .= C by RUSUB_1:def 3;

        hence thesis;

      end;

      hence thesis by LATTICES:def 14;

    end;

    theorem :: RUSUB_2:57

    

     Th57: for V be RealUnitarySpace holds LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #) is 01_Lattice

    proof

      let V be RealUnitarySpace;

       LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #) is lower-bounded upper-bounded Lattice by Th55, Th56;

      hence thesis;

    end;

    theorem :: RUSUB_2:58

    

     Th58: for V be RealUnitarySpace holds LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #) is modular

    proof

      let V be RealUnitarySpace;

      set S = LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #);

      for A,B,C be Element of S st A [= C holds (A "\/" (B "/\" C)) = ((A "\/" B) "/\" C)

      proof

        let A,B,C be Element of S;

        reconsider W1 = A, W2 = B, W3 = C as strict Subspace of V by Def3;

        assume

         A1: A [= C;

        reconsider AB = (W1 + W2) as Element of S by Def3;

        reconsider BC = (W2 /\ W3) as Element of S by Def3;

        (W1 + W3) = (( SubJoin V) . (A,C)) by Def7

        .= (A "\/" C) by LATTICES:def 1

        .= W3 by A1, LATTICES:def 3;

        then

         A2: W1 is Subspace of W3 by Th8;

        

        thus (A "\/" (B "/\" C)) = (( SubJoin V) . (A,(B "/\" C))) by LATTICES:def 1

        .= (( SubJoin V) . (A,(( SubMeet V) . (B,C)))) by LATTICES:def 2

        .= (( SubJoin V) . (A,BC)) by Def8

        .= (W1 + (W2 /\ W3)) by Def7

        .= ((W1 + W2) /\ W3) by A2, Th29

        .= (( SubMeet V) . (AB,C)) by Def8

        .= (( SubMeet V) . ((( SubJoin V) . (A,B)),C)) by Def7

        .= (( SubMeet V) . ((A "\/" B),C)) by LATTICES:def 1

        .= ((A "\/" B) "/\" C) by LATTICES:def 2;

      end;

      hence thesis by LATTICES:def 12;

    end;

    theorem :: RUSUB_2:59

    

     Th59: for V be RealUnitarySpace holds LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #) is complemented

    proof

      let V be RealUnitarySpace;

      reconsider S = LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #) as 01_Lattice by Th57;

      reconsider S0 = S as 0_Lattice;

      reconsider S1 = S as 1_Lattice;

      reconsider Z = ( (0). V), I = ( (Omega). V) as Element of S by Def3;

      reconsider Z0 = Z as Element of S0;

      reconsider I1 = I as Element of S1;

      now

        let A be Element of S0;

        reconsider W = A as Subspace of V by Def3;

        

        thus (A "/\" Z0) = (( SubMeet V) . (A,Z0)) by LATTICES:def 2

        .= (W /\ ( (0). V)) by Def8

        .= Z0 by Th18;

      end;

      then

       A1: ( Bottom S) = Z by RLSUB_2: 64;

      now

        let A be Element of S1;

        reconsider W = A as Subspace of V by Def3;

        

        thus (A "\/" I1) = (( SubJoin V) . (A,I1)) by LATTICES:def 1

        .= (W + ( (Omega). V)) by Def7

        .= the UNITSTR of V by Th11

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

      end;

      then

       A2: ( Top S) = I by RLSUB_2: 65;

      now

        let A be Element of S;

        reconsider W = A as Subspace of V by Def3;

        set L = the strict Linear_Compl of W;

        reconsider B9 = L as Element of S by Def3;

        take B = B9;

        

         A3: (B "/\" A) = (( SubMeet V) . (B,A)) by LATTICES:def 2

        .= (L /\ W) by Def8

        .= ( Bottom S) by A1, Th37;

        (B "\/" A) = (( SubJoin V) . (B,A)) by LATTICES:def 1

        .= (L + W) by Def7

        .= the UNITSTR of V by Th36

        .= ( Top S) by A2, RUSUB_1:def 3;

        hence B is_a_complement_of A by A3, LATTICES:def 18;

      end;

      hence thesis by LATTICES:def 19;

    end;

    registration

      let V be RealUnitarySpace;

      cluster LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #) -> lower-bounded upper-bounded modular complemented;

      coherence by Th55, Th56, Th58, Th59;

    end

    theorem :: RUSUB_2:60

    for V be RealUnitarySpace, W1,W2,W3 be strict Subspace of V holds W1 is Subspace of W2 implies (W1 /\ W3) is Subspace of (W2 /\ W3)

    proof

      let V be RealUnitarySpace, W1,W2,W3 be strict Subspace of V;

      set S = LattStr (# ( Subspaces V), ( SubJoin V), ( SubMeet V) #);

      reconsider A = W1, B = W2, C = W3, AC = (W1 /\ W3), BC = (W2 /\ W3) as Element of S by Def3;

      assume

       A1: W1 is Subspace of W2;

      (A "\/" B) = (( SubJoin V) . (A,B)) by LATTICES:def 1

      .= (W1 + W2) by Def7

      .= B by A1, Th8;

      then A [= B by LATTICES:def 3;

      then (A "/\" C) [= (B "/\" C) by LATTICES: 9;

      then

       A2: ((A "/\" C) "\/" (B "/\" C)) = (B "/\" C) by LATTICES:def 3;

      

       A3: (B "/\" C) = (( SubMeet V) . (B,C)) by LATTICES:def 2

      .= (W2 /\ W3) by Def8;

      ((A "/\" C) "\/" (B "/\" C)) = (( SubJoin V) . ((A "/\" C),(B "/\" C))) by LATTICES:def 1

      .= (( SubJoin V) . ((( SubMeet V) . (A,C)),(B "/\" C))) by LATTICES:def 2

      .= (( SubJoin V) . ((( SubMeet V) . (A,C)),(( SubMeet V) . (B,C)))) by LATTICES:def 2

      .= (( SubJoin V) . ((( SubMeet V) . (A,C)),BC)) by Def8

      .= (( SubJoin V) . (AC,BC)) by Def8

      .= ((W1 /\ W3) + (W2 /\ W3)) by Def7;

      hence thesis by A2, A3, Th8;

    end;

    begin

    theorem :: RUSUB_2:61

    for V be RealUnitarySpace, W be strict Subspace of V holds (for v be VECTOR of V holds v in W) implies W = the UNITSTR of V by Lm12;

    theorem :: RUSUB_2:62

    for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V holds ex C be Coset of W st v in C by Lm17;

    theorem :: RUSUB_2:63

    for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V, x be set holds x in (v + W) iff ex u be VECTOR of V st u in W & x = (v + u) by Lm16;