rusub_1.miz



    begin

    definition

      let V be RealUnitarySpace;

      :: RUSUB_1:def1

      mode Subspace of V -> RealUnitarySpace means

      : Def1: the carrier of it c= the carrier of V & ( 0. it ) = ( 0. V) & the addF of it = (the addF of V || the carrier of it ) & the Mult of it = (the Mult of V | [: REAL , the carrier of it :]) & the scalar of it = (the scalar of V || the carrier of it );

      existence

      proof

        take V;

        

         A1: ( dom the scalar of V) = [:the carrier of V, the carrier of V:] by FUNCT_2:def 1;

        ( dom the addF of V) = [:the carrier of V, the carrier of V:] & ( dom the Mult of V) = [: REAL , the carrier of V:] by FUNCT_2:def 1;

        hence thesis by A1, RELAT_1: 69;

      end;

    end

    theorem :: RUSUB_1:1

    for V be RealUnitarySpace, W1,W2 be Subspace of V, x be object st x in W1 & W1 is Subspace of W2 holds x in W2

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      let x be object;

      assume x in W1 & W1 is Subspace of W2;

      then x in the carrier of W1 & the carrier of W1 c= the carrier of W2 by Def1;

      hence thesis;

    end;

    theorem :: RUSUB_1:2

    

     Th2: for V be RealUnitarySpace, W be Subspace of V, x be object st x in W holds x in V

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let x be object;

      assume x in W;

      then

       A1: x in the carrier of W;

      the carrier of W c= the carrier of V by Def1;

      hence thesis by A1;

    end;

    theorem :: RUSUB_1:3

    

     Th3: for V be RealUnitarySpace, W be Subspace of V, w be VECTOR of W holds w is VECTOR of V

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let w be VECTOR of W;

      w in V by Th2, RLVECT_1: 1;

      hence thesis;

    end;

    theorem :: RUSUB_1:4

    for V be RealUnitarySpace, W be Subspace of V holds ( 0. W) = ( 0. V) by Def1;

    theorem :: RUSUB_1:5

    for V be RealUnitarySpace, W1,W2 be Subspace of V holds ( 0. W1) = ( 0. W2)

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      ( 0. W1) = ( 0. V) by Def1;

      hence thesis by Def1;

    end;

    theorem :: RUSUB_1:6

    

     Th6: for V be RealUnitarySpace, W be Subspace of V, u,v be VECTOR of V, w1,w2 be VECTOR of W st w1 = v & w2 = u holds (w1 + w2) = (v + u)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let u,v be VECTOR of V;

      let w1,w2 be VECTOR of W;

      assume

       A1: v = w1 & u = w2;

      (w1 + w2) = ((the addF of V || the carrier of W) . [w1, w2]) by Def1;

      hence thesis by A1, FUNCT_1: 49;

    end;

    theorem :: RUSUB_1:7

    

     Th7: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V, w be VECTOR of W, a be Real st w = v holds (a * w) = (a * v)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      let w be VECTOR of W;

      let a be Real;

      assume

       A1: w = v;

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

      (aa * w) = ((the Mult of V | [: REAL , the carrier of W:]) . [aa, w]) by Def1;

      hence thesis by A1, FUNCT_1: 49;

    end;

    theorem :: RUSUB_1:8

    for V be RealUnitarySpace, W be Subspace of V, v1,v2 be VECTOR of V, w1,w2 be VECTOR of W st w1 = v1 & w2 = v2 holds (w1 .|. w2) = (v1 .|. v2)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v1,v2 be VECTOR of V;

      let w1,w2 be VECTOR of W;

      reconsider ww1 = w1, ww2 = w2 as VECTOR of V by Th3;

      assume w1 = v1 & w2 = v2;

      then

       A1: (v1 .|. v2) = (the scalar of V . [ww1, ww2]);

      (w1 .|. w2) = (the scalar of W . [w1, w2])

      .= ((the scalar of V || the carrier of W) . [w1, w2]) by Def1;

      hence thesis by A1, FUNCT_1: 49;

    end;

    theorem :: RUSUB_1:9

    

     Th9: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V, w be VECTOR of W st w = v holds ( - v) = ( - w)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      let w be VECTOR of W;

      

       A1: ( - v) = (( - 1) * v) & ( - w) = (( - 1) * w) by RLVECT_1: 16;

      assume w = v;

      hence thesis by A1, Th7;

    end;

    theorem :: RUSUB_1:10

    

     Th10: for V be RealUnitarySpace, W be Subspace of V, u,v be VECTOR of V, w1,w2 be VECTOR of W st w1 = v & w2 = u holds (w1 - w2) = (v - u)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let u,v be VECTOR of V;

      let w1,w2 be VECTOR of W;

      assume that

       A1: w1 = v and

       A2: w2 = u;

      ( - w2) = ( - u) by A2, Th9;

      hence thesis by A1, Th6;

    end;

    theorem :: RUSUB_1:11

    

     Th11: for V be RealUnitarySpace, W be Subspace of V holds ( 0. V) in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      ( 0. W) in W;

      hence thesis by Def1;

    end;

    theorem :: RUSUB_1:12

    for V be RealUnitarySpace, W1,W2 be Subspace of V holds ( 0. W1) in W2

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      ( 0. W1) = ( 0. V) by Def1;

      hence thesis by Th11;

    end;

    theorem :: RUSUB_1:13

    for V be RealUnitarySpace, W be Subspace of V holds ( 0. W) in V by Th2, RLVECT_1: 1;

    

     Lm1: for V be RealUnitarySpace, W be Subspace of V, V1,V2 be Subset of V st the carrier of W = V1 holds V1 is linearly-closed

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let V1,V2 be Subset of V;

      set VW = the carrier of W;

      reconsider WW = W as RealUnitarySpace;

      assume

       A1: the carrier of W = V1;

      

       A2: for a be Real, v be VECTOR of V st v in V1 holds (a * v) in V1

      proof

        let a be Real, v be VECTOR of V;

        assume v in V1;

        then

        reconsider vv = v as VECTOR of WW by A1;

        reconsider vw = (a * vv) as Element of VW;

        vw in V1 by A1;

        hence thesis by Th7;

      end;

      for v,u be VECTOR of V st v in V1 & u in V1 holds (v + u) in V1

      proof

        let v,u be VECTOR of V;

        assume v in V1 & u in V1;

        then

        reconsider vv = v, uu = u as VECTOR of WW by A1;

        reconsider vw = (vv + uu) as Element of VW;

        vw in V1 by A1;

        hence thesis by Th6;

      end;

      hence thesis by A2, RLSUB_1:def 1;

    end;

    theorem :: RUSUB_1:14

    

     Th14: for V be RealUnitarySpace, W be Subspace of V, u,v be VECTOR of V st u in W & v in W holds (u + v) in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      reconsider VW = the carrier of W as Subset of V by Def1;

      let u,v be VECTOR of V;

      assume u in W & v in W;

      then

       A1: u in the carrier of W & v in the carrier of W;

      VW is linearly-closed by Lm1;

      then (u + v) in the carrier of W by A1, RLSUB_1:def 1;

      hence thesis;

    end;

    theorem :: RUSUB_1:15

    

     Th15: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V, a be Real st v in W holds (a * v) in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      reconsider VW = the carrier of W as Subset of V by Def1;

      let v be VECTOR of V;

      let a be Real;

      assume v in W;

      then

       A1: v in the carrier of W;

      reconsider aa = a as Real;

      VW is linearly-closed by Lm1;

      then (aa * v) in the carrier of W by A1, RLSUB_1:def 1;

      hence thesis;

    end;

    theorem :: RUSUB_1:16

    

     Th16: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V st v in W holds ( - v) in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      assume v in W;

      then (( - 1) * v) in W by Th15;

      hence thesis by RLVECT_1: 16;

    end;

    theorem :: RUSUB_1:17

    

     Th17: for V be RealUnitarySpace, W be Subspace of V, u,v be VECTOR of V st u in W & v in W holds (u - v) in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let u,v be VECTOR of V;

      assume that

       A1: u in W and

       A2: v in W;

      ( - v) in W by A2, Th16;

      hence thesis by A1, Th14;

    end;

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

    theorem :: RUSUB_1:18

    

     Th18: for V be RealUnitarySpace, V1 be Subset of V, D be non empty set, d1 be Element of D, A be BinOp of D, M be Function of [: REAL , D:], D, S be Function of [:D, D:], REAL st V1 = D & d1 = ( 0. V) & A = (the addF of V || V1) & M = (the Mult of V | [: REAL , V1:]) & S = (the scalar of V || V1) holds UNITSTR (# D, d1, A, M, S #) is Subspace of V

    proof

      let V be RealUnitarySpace;

      let V1 be Subset of V;

      let D be non empty set;

      let d1 be Element of D;

      let A be BinOp of D;

      let M be Function of [: REAL , D:], D;

      let S be Function of [:D, D:], REAL ;

      assume that

       A1: V1 = D and

       A2: d1 = ( 0. V) and

       A3: A = (the addF of V || V1) and

       A4: M = (the Mult of V | [: REAL , V1:]) and

       A5: S = (the scalar of V || V1);

       UNITSTR (# D, d1, A, M, S #) is Subspace of V

      proof

        set W = UNITSTR (# D, d1, A, M, S #);

        

         A6: for a be Real, x be VECTOR of W holds (a * x) = (the Mult of V . [a, x])

        proof

          let a be Real, x be VECTOR of W;

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

          (a * x) = (the Mult of V . [a, x]) by A1, A4, FUNCT_1: 49;

          hence thesis;

        end;

        

         A7: for x,y be VECTOR of W holds (x .|. y) = (the scalar of V . [x, y]) by A1, A5, FUNCT_1: 49;

        

         A8: for x,y be VECTOR of W holds (x + y) = (the addF of V . [x, y]) by A1, A3, FUNCT_1: 49;

        

         A9: W is RealUnitarySpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable

        proof

          set SV = the scalar of V;

          set MV = the Mult of V;

          set AV = the addF of V;

          

           A10: for x be VECTOR of W holds (jj * x) = x

          proof

            let x be VECTOR of W;

            reconsider y = x as VECTOR of V by A1, TARSKI:def 3;

            

            thus (jj * x) = (jj * y) by A6

            .= x by RLVECT_1:def 8;

          end;

          

           A11: for a,b be Real, x be VECTOR of W holds ((a * b) * x) = (a * (b * x))

          proof

            let a,b be Real;

            let x be VECTOR of W;

            reconsider y = x as VECTOR of V by A1, TARSKI:def 3;

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

            ((a * b) * x) = ((a * b) * y) by A6

            .= (a * (b * y)) by RLVECT_1:def 7

            .= (MV . [a, (b * x)]) by A6

            .= (a * (b * x)) by A1, A4, FUNCT_1: 49;

            hence thesis;

          end;

          

           A12: for a be Real, x,y be VECTOR of W holds (a * (x + y)) = ((a * x) + (a * y))

          proof

            let a be Real;

            let x,y be VECTOR of W;

            reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;

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

            (a * (x + y)) = (MV . [a, (x + y)]) by A1, A4, FUNCT_1: 49

            .= (a * (x1 + y1)) by A8

            .= ((a * x1) + (a * y1)) by RLVECT_1:def 5

            .= (AV . [(MV . [a, x1]), (a * y)]) by A6

            .= (AV . [(a * x), (a * y)]) by A6

            .= ((a * x) + (a * y)) by A1, A3, FUNCT_1: 49;

            hence thesis;

          end;

          

           A13: for x be VECTOR of W holds (x + ( 0. W)) = x

          proof

            let x be VECTOR of W;

            reconsider y = x as VECTOR of V by A1, TARSKI:def 3;

            

            thus (x + ( 0. W)) = (y + ( 0. V)) by A2, A8

            .= x by RLVECT_1: 4;

          end;

          thus W is RealUnitarySpace-like

          proof

            let x,y,z be VECTOR of W;

            reconsider z1 = z as VECTOR of V by A1, TARSKI:def 3;

            reconsider y1 = y as VECTOR of V by A1, TARSKI:def 3;

            reconsider x1 = x as VECTOR of V by A1, TARSKI:def 3;

            let a be Real;

            

             A14: x = ( 0. W) implies (x .|. x) = 0

            proof

              assume x = ( 0. W);

              then (x1 .|. x1) = 0 by A2, BHSP_1:def 2;

              then (SV . [x1, x1]) = 0 ;

              hence thesis by A7;

            end;

            (x .|. x) = 0 implies x = ( 0. W)

            proof

              assume (x .|. x) = 0 ;

              then (SV . [x1, x1]) = 0 by A7;

              then (x1 .|. x1) = 0 ;

              hence thesis by A2, BHSP_1:def 2;

            end;

            hence (x .|. x) = 0 iff x = ( 0. W) by A14;

             0 <= (x1 .|. x1) by BHSP_1:def 2;

            then 0 <= (SV . [x1, x1]);

            hence 0 <= (x .|. x) by A7;

            (SV . [x1, y1]) = (y1 .|. x1) by BHSP_1:def 1;

            then (SV . [x1, y1]) = (SV . [y1, x1]);

            then (x .|. y) = (SV . [y1, x1]) by A7;

            hence (x .|. y) = (y .|. x) by A7;

            

             A15: ((x + y) .|. z) = (SV . [(x + y), z]) by A7

            .= (SV . [(x1 + y1), z]) by A8

            .= ((x1 + y1) .|. z1)

            .= ((x1 .|. z1) + (y1 .|. z1)) by BHSP_1:def 2;

            ((x .|. z) + (y .|. z)) = ((SV . [x, z]) + (y .|. z)) by A7

            .= ((SV . [x, z]) + (SV . [y, z])) by A7

            .= ((x1 .|. z1) + (y1 .|. z1));

            hence ((x + y) .|. z) = ((x .|. z) + (y .|. z)) by A15;

            

             A16: (a * (x .|. y)) = (a * (SV . [x, y])) by A7

            .= (a * (x1 .|. y1));

            ((a * x) .|. y) = (SV . [(a * x), y]) by A7

            .= (SV . [(a * x1), y]) by A6

            .= ((a * x1) .|. y1)

            .= (a * (x1 .|. y1)) by BHSP_1:def 2;

            hence thesis by A16;

          end;

          

           A17: for a,b be Real, x be VECTOR of W holds ((a + b) * x) = ((a * x) + (b * x))

          proof

            let a,b be Real;

            let x be VECTOR of W;

            reconsider y = x as VECTOR of V by A1, TARSKI:def 3;

            reconsider a, b as Real;

            ((a + b) * x) = ((a + b) * y) by A6

            .= ((a * y) + (b * y)) by RLVECT_1:def 6

            .= (AV . [(MV . [a, y]), (b * x)]) by A6

            .= (AV . [(a * x), (b * x)]) by A6

            .= ((a * x) + (b * x)) by A1, A3, FUNCT_1: 49;

            hence thesis;

          end;

          

           A18: W is right_complementable

          proof

            let x be VECTOR of W;

            reconsider x1 = x as VECTOR of V by A1, TARSKI:def 3;

            consider v be VECTOR of V such that

             A19: (x1 + v) = ( 0. V) by ALGSTR_0:def 11;

            v = ( - x1) by A19, RLVECT_1:def 10

            .= (( - 1) * x1) by RLVECT_1: 16

            .= (( - jj) * x) by A6;

            then

            reconsider y = v as VECTOR of W;

            take y;

            thus thesis by A2, A8, A19;

          end;

          

           A20: for x,y be Element of W holds (x + y) = (y + x)

          proof

            let x,y be Element of W;

            reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;

            

            thus (x + y) = (x1 + y1) by A8

            .= (y1 + x1)

            .= (y + x) by A8;

          end;

          for x,y,z be VECTOR of W holds ((x + y) + z) = (x + (y + z))

          proof

            let x,y,z be VECTOR of W;

            reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1, TARSKI:def 3;

            

            thus ((x + y) + z) = (AV . [(x + y), z1]) by A8

            .= ((x1 + y1) + z1) by A8

            .= (x1 + (y1 + z1)) by RLVECT_1:def 3

            .= (AV . [x1, (y + z)]) by A8

            .= (x + (y + z)) by A8;

          end;

          hence thesis by A20, A13, A18, A12, A17, A11, A10;

        end;

        ( 0. W) = ( 0. V) by A2;

        hence thesis by A1, A3, A4, A5, A9, Def1;

      end;

      hence thesis;

    end;

    theorem :: RUSUB_1:19

    

     Th19: for V be RealUnitarySpace holds V is Subspace of V

    proof

      let V be RealUnitarySpace;

      thus the carrier of V c= the carrier of V & ( 0. V) = ( 0. V);

      thus thesis by RELSET_1: 19;

    end;

    theorem :: RUSUB_1:20

    

     Th20: for V,X be strict RealUnitarySpace holds V is Subspace of X & X is Subspace of V implies V = X

    proof

      let V,X be strict RealUnitarySpace;

      assume that

       A1: V is Subspace of X and

       A2: X is Subspace of V;

      set VX = the carrier of X;

      set VV = the carrier of V;

      VV c= VX & VX c= VV by A1, A2, Def1;

      then

       A3: VV = VX;

      set MX = the Mult of X;

      set MV = the Mult of V;

      MV = (MX | [: REAL , VV:]) & MX = (MV | [: REAL , VX:]) by A1, A2, Def1;

      then

       A4: MV = MX by A3, RELAT_1: 72;

      set AX = the addF of X;

      set AV = the addF of V;

      AV = (AX || VV) & AX = (AV || VX) by A1, A2, Def1;

      then

       A5: AV = AX by A3, RELAT_1: 72;

      set SX = the scalar of X;

      set SV = the scalar of V;

      

       A6: SX = (SV || VX) by A2, Def1;

      ( 0. V) = ( 0. X) & SV = (SX || VV) by A1, Def1;

      hence thesis by A3, A5, A4, A6, RELAT_1: 72;

    end;

    theorem :: RUSUB_1:21

    

     Th21: for V,X,Y be RealUnitarySpace st V is Subspace of X & X is Subspace of Y holds V is Subspace of Y

    proof

      let V,X,Y be RealUnitarySpace;

      assume that

       A1: V is Subspace of X and

       A2: X is Subspace of Y;

      the carrier of V c= the carrier of X & the carrier of X c= the carrier of Y by A1, A2, Def1;

      hence the carrier of V c= the carrier of Y;

      ( 0. V) = ( 0. X) by A1, Def1;

      hence ( 0. V) = ( 0. Y) by A2, Def1;

      thus the addF of V = (the addF of Y || the carrier of V)

      proof

        set AY = the addF of Y;

        set VX = the carrier of X;

        set AX = the addF of X;

        set VV = the carrier of V;

        set AV = the addF of V;

        VV c= VX by A1, Def1;

        then

         A3: [:VV, VV:] c= [:VX, VX:] by ZFMISC_1: 96;

        AV = (AX || VV) by A1, Def1;

        then AV = ((AY || VX) || VV) by A2, Def1;

        hence thesis by A3, FUNCT_1: 51;

      end;

      thus the Mult of V = (the Mult of Y | [: REAL , the carrier of V:])

      proof

        set MY = the Mult of Y;

        set VX = the carrier of X;

        set MX = the Mult of X;

        set VV = the carrier of V;

        set MV = the Mult of V;

        VV c= VX by A1, Def1;

        then

         A4: [: REAL , VV:] c= [: REAL , VX:] by ZFMISC_1: 95;

        MV = (MX | [: REAL , VV:]) by A1, Def1;

        then MV = ((MY | [: REAL , VX:]) | [: REAL , VV:]) by A2, Def1;

        hence thesis by A4, FUNCT_1: 51;

      end;

      set SY = the scalar of Y;

      set SX = the scalar of X;

      set SV = the scalar of V;

      set VX = the carrier of X;

      set VV = the carrier of V;

      VV c= VX by A1, Def1;

      then

       A5: [:VV, VV:] c= [:VX, VX:] by ZFMISC_1: 96;

      SV = (SX || VV) by A1, Def1;

      then SV = ((SY || VX) || VV) by A2, Def1;

      hence thesis by A5, FUNCT_1: 51;

    end;

    theorem :: RUSUB_1:22

    

     Th22: for V be RealUnitarySpace, W1,W2 be Subspace of V st the carrier of W1 c= the carrier of W2 holds W1 is Subspace of W2

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      set VW1 = the carrier of W1;

      set VW2 = the carrier of W2;

      set AV = the addF of V;

      set MV = the Mult of V;

      set SV = the scalar of V;

      assume

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

      then

       A2: [:VW1, VW1:] c= [:VW2, VW2:] by ZFMISC_1: 96;

      ( 0. W1) = ( 0. V) by Def1;

      hence the carrier of W1 c= the carrier of W2 & ( 0. W1) = ( 0. W2) by A1, Def1;

      the addF of W1 = (AV || VW1) & the addF of W2 = (AV || VW2) by Def1;

      hence the addF of W1 = (the addF of W2 || the carrier of W1) by A2, FUNCT_1: 51;

      

       A3: [: REAL , VW1:] c= [: REAL , VW2:] by A1, ZFMISC_1: 95;

      the Mult of W1 = (MV | [: REAL , VW1:]) & the Mult of W2 = (MV | [: REAL , VW2:]) by Def1;

      hence the Mult of W1 = (the Mult of W2 | [: REAL , the carrier of W1:]) by A3, FUNCT_1: 51;

      

       A4: [:VW1, VW1:] c= [:VW2, VW2:] by A1, ZFMISC_1: 96;

      the scalar of W1 = (SV || VW1) & the scalar of W2 = (SV || VW2) by Def1;

      hence thesis by A4, FUNCT_1: 51;

    end;

    theorem :: RUSUB_1:23

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

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      assume

       A1: for v be VECTOR of V st v in W1 holds v in W2;

      the carrier of W1 c= the carrier of W2

      proof

        let x be object;

        assume

         A2: x in the carrier of W1;

        the carrier of W1 c= the carrier of V by Def1;

        then

        reconsider v = x as VECTOR of V by A2;

        v in W1 by A2;

        then v in W2 by A1;

        hence thesis;

      end;

      hence thesis by Th22;

    end;

    registration

      let V be RealUnitarySpace;

      cluster strict for Subspace of V;

      existence

      proof

        the carrier of V is Subset of V iff the carrier of V c= the carrier of V;

        then

        reconsider V1 = the carrier of V as Subset of V;

        

         A1: the scalar of V = (the scalar of V || V1) by RELSET_1: 19;

        the addF of V = (the addF of V || V1) & the Mult of V = (the Mult of V | [: REAL , V1:]) by RELSET_1: 19;

        then UNITSTR (# the carrier of V, ( 0. V), the addF of V, the Mult of V, the scalar of V #) is Subspace of V by A1, Th18;

        hence thesis;

      end;

    end

    theorem :: RUSUB_1:24

    

     Th24: for V be RealUnitarySpace, W1,W2 be strict Subspace of V st the carrier of W1 = the carrier of W2 holds W1 = W2

    proof

      let V be RealUnitarySpace;

      let W1,W2 be strict Subspace of V;

      assume the carrier of W1 = the carrier of W2;

      then W1 is Subspace of W2 & W2 is Subspace of W1 by Th22;

      hence thesis by Th20;

    end;

    theorem :: RUSUB_1:25

    

     Th25: for V be RealUnitarySpace, W1,W2 be strict Subspace of V st (for v be VECTOR of V holds v in W1 iff v in W2) holds W1 = W2

    proof

      let V be RealUnitarySpace;

      let W1,W2 be strict Subspace of V;

      assume

       A1: for v be VECTOR of V holds v in W1 iff v in W2;

      for x be object holds x in the carrier of W1 iff x in the carrier of W2

      proof

        let x be object;

        thus x in the carrier of W1 implies x in the carrier of W2

        proof

          assume

           A2: x in the carrier of W1;

          the carrier of W1 c= the carrier of V by Def1;

          then

          reconsider v = x as VECTOR of V by A2;

          v in W1 by A2;

          then v in W2 by A1;

          hence thesis;

        end;

        assume

         A3: x in the carrier of W2;

        the carrier of W2 c= the carrier of V by Def1;

        then

        reconsider v = x as VECTOR of V by A3;

        v in W2 by A3;

        then v in W1 by A1;

        hence thesis;

      end;

      then the carrier of W1 = the carrier of W2 by TARSKI: 2;

      hence thesis by Th24;

    end;

    theorem :: RUSUB_1:26

    for V be strict RealUnitarySpace, W be strict Subspace of V st the carrier of W = the carrier of V holds W = V

    proof

      let V be strict RealUnitarySpace;

      let W be strict Subspace of V;

      assume

       A1: the carrier of W = the carrier of V;

      V is Subspace of V by Th19;

      hence thesis by A1, Th24;

    end;

    theorem :: RUSUB_1:27

    for V be strict RealUnitarySpace, W be strict Subspace of V st (for v be VECTOR of V holds v in W iff v in V) holds W = V

    proof

      let V be strict RealUnitarySpace;

      let W be strict Subspace of V;

      assume

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

      V is Subspace of V by Th19;

      hence thesis by A1, Th25;

    end;

    theorem :: RUSUB_1:28

    for V be RealUnitarySpace, W be Subspace of V, V1 be Subset of V st the carrier of W = V1 holds V1 is linearly-closed by Lm1;

    theorem :: RUSUB_1:29

    

     Th29: for V be RealUnitarySpace, V1 be Subset of V st V1 <> {} & V1 is linearly-closed holds ex W be strict Subspace of V st V1 = the carrier of W

    proof

      let V be RealUnitarySpace;

      let V1 be Subset of V;

      assume that

       A1: V1 <> {} and

       A2: V1 is linearly-closed;

      reconsider D = V1 as non empty set by A1;

      reconsider d1 = ( 0. V) as Element of D by A2, RLSUB_1: 1;

      set S = (the scalar of V || V1);

      set VV = the carrier of V;

      set M = (the Mult of V | [: REAL , V1:]);

      ( dom the Mult of V) = [: REAL , VV:] by FUNCT_2:def 1;

      then

       A3: ( dom M) = ( [: REAL , VV:] /\ [: REAL , V1:]) by RELAT_1: 61;

       [: REAL , V1:] c= [: REAL , VV:] by ZFMISC_1: 95;

      then

       A4: ( dom M) = [: REAL , D:] by A3, XBOOLE_1: 28;

      now

        let y be object;

        thus y in D implies ex x be object st x in ( dom M) & y = (M . x)

        proof

          assume

           A5: y in D;

          then

          reconsider v1 = y as Element of VV;

          

           A6: [jj, y] in [: REAL , D:] by A5, ZFMISC_1: 87;

          

          then (M . [1, y]) = (1 * v1) by FUNCT_1: 49

          .= y by RLVECT_1:def 8;

          hence thesis by A4, A6;

        end;

        given x be object such that

         A7: x in ( dom M) and

         A8: y = (M . x);

        consider x1,x2 be object such that

         A9: x1 in REAL and

         A10: x2 in D and

         A11: x = [x1, x2] by A4, A7, ZFMISC_1:def 2;

        reconsider xx1 = x1 as Real by A9;

        reconsider v2 = x2 as Element of VV by A10;

         [x1, x2] in [: REAL , V1:] by A9, A10, ZFMISC_1: 87;

        then y = (xx1 * v2) by A8, A11, FUNCT_1: 49;

        hence y in D by A2, A10, RLSUB_1:def 1;

      end;

      then D = ( rng M) by FUNCT_1:def 3;

      then

      reconsider M as Function of [: REAL , D:], D by A4, FUNCT_2:def 1, RELSET_1: 4;

      set A = (the addF of V || V1);

      ( dom the addF of V) = [:VV, VV:] by FUNCT_2:def 1;

      then

       A12: ( dom A) = ( [:VV, VV:] /\ [:V1, V1:]) by RELAT_1: 61;

      then

      reconsider S as Function of [:D, D:], REAL by FUNCT_2: 32;

      

       A13: ( dom A) = [:D, D:] by A12, XBOOLE_1: 28;

      now

        let y be object;

        thus y in D implies ex x be object st x in ( dom A) & y = (A . x)

        proof

          assume

           A14: y in D;

          then

          reconsider v1 = y, v0 = d1 as Element of VV;

          

           A15: [d1, y] in [:D, D:] by A14, ZFMISC_1: 87;

          

          then (A . [d1, y]) = (v0 + v1) by FUNCT_1: 49

          .= y by RLVECT_1: 4;

          hence thesis by A13, A15;

        end;

        given x be object such that

         A16: x in ( dom A) and

         A17: y = (A . x);

        consider x1,x2 be object such that

         A18: x1 in D & x2 in D and

         A19: x = [x1, x2] by A13, A16, ZFMISC_1:def 2;

        reconsider v1 = x1, v2 = x2 as Element of VV by A18;

         [x1, x2] in [:V1, V1:] by A18, ZFMISC_1: 87;

        then y = (v1 + v2) by A17, A19, FUNCT_1: 49;

        hence y in D by A2, A18, RLSUB_1:def 1;

      end;

      then D = ( rng A) by FUNCT_1:def 3;

      then

      reconsider A as Function of [:D, D:], D by A13, FUNCT_2:def 1, RELSET_1: 4;

      set W = UNITSTR (# D, d1, A, M, S #);

      W is Subspace of V by Th18;

      hence thesis;

    end;

    begin

    definition

      let V be RealUnitarySpace;

      :: RUSUB_1:def2

      func (0). V -> strict Subspace of V means

      : Def2: the carrier of it = {( 0. V)};

      correctness by Th24, Th29, RLSUB_1: 4;

    end

    definition

      let V be RealUnitarySpace;

      :: RUSUB_1:def3

      func (Omega). V -> strict Subspace of V equals the UNITSTR of V;

      coherence

      proof

        set W = the UNITSTR of V;

        

         A1: for u,v,w be VECTOR of W holds ((u + v) + w) = (u + (v + w))

        proof

          let u,v,w be VECTOR of W;

          reconsider u9 = u, v9 = v, w9 = w as VECTOR of V;

          

          thus ((u + v) + w) = ((u9 + v9) + w9)

          .= (u9 + (v9 + w9)) by RLVECT_1:def 3

          .= (u + (v + w));

        end;

        

         A2: for v be VECTOR of W holds (v + ( 0. W)) = v

        proof

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          

          thus (v + ( 0. W)) = (v9 + ( 0. V))

          .= v by RLVECT_1: 4;

        end;

        

         A3: W is right_complementable

        proof

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          consider w9 be VECTOR of V such that

           A4: (v9 + w9) = ( 0. V) by ALGSTR_0:def 11;

          reconsider w = w9 as VECTOR of W;

          take w;

          thus thesis by A4;

        end;

        

         A5: for v be VECTOR of W holds (jj * v) = v

        proof

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          

          thus (jj * v) = (1 * v9)

          .= v by RLVECT_1:def 8;

        end;

        

         A6: for a,b be Real, v be VECTOR of W holds ((a + b) * v) = ((a * v) + (b * v))

        proof

          let a,b be Real;

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          

          thus ((a + b) * v) = ((a + b) * v9)

          .= ((a * v9) + (b * v9)) by RLVECT_1:def 6

          .= ((a * v) + (b * v));

        end;

        

         A7: for a be Real, v,w be VECTOR of W holds (a * (v + w)) = ((a * v) + (a * w))

        proof

          let a be Real;

          let v,w be VECTOR of W;

          reconsider v9 = v, w9 = w as VECTOR of V;

          

          thus (a * (v + w)) = (a * (v9 + w9))

          .= ((a * v9) + (a * w9)) by RLVECT_1:def 5

          .= ((a * v) + (a * w));

        end;

        

         A8: for a be Real, v,w be VECTOR of W, v9,w9 be VECTOR of V st v = v9 & w = w9 holds (v + w) = (v9 + w9) & (a * v) = (a * v9) & (v .|. w) = (v9 .|. w9);

        

         A9: for v,w be VECTOR of W holds (v + w) = (w + v)

        proof

          let v,w be VECTOR of W;

          reconsider v9 = v, w9 = w as VECTOR of V;

          

          thus (v + w) = (w9 + v9) by A8

          .= (w + v);

        end;

        

         A10: ( 0. W) = ( 0. V);

        

         A11: W is RealUnitarySpace-like

        proof

          let x,y,z be VECTOR of W;

          let a be Real;

          reconsider x9 = x as VECTOR of V;

          reconsider y9 = y as VECTOR of V;

          reconsider z9 = z as VECTOR of V;

          

           A12: ((x + y) .|. z) = ((x9 + y9) .|. z9)

          .= ((x9 .|. z9) + (y9 .|. z9)) by BHSP_1:def 2;

          (x9 .|. x9) = (x .|. x);

          hence (x .|. x) = 0 iff x = ( 0. W) by A10, BHSP_1:def 2;

          (x9 .|. x9) = (x .|. x);

          hence 0 <= (x .|. x) by BHSP_1:def 2;

          (x9 .|. y9) = (x .|. y);

          hence (x .|. y) = (y .|. x) by A8;

          thus ((x + y) .|. z) = ((x .|. z) + (y .|. z)) by A12;

          ((a * x) .|. y) = ((a * x9) .|. y9)

          .= (a * (x9 .|. y9)) by BHSP_1:def 2;

          hence ((a * x) .|. y) = (a * (x .|. y));

        end;

        for a,b be Real, v be VECTOR of W holds ((a * b) * v) = (a * (b * v))

        proof

          let a,b be Real;

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          

          thus ((a * b) * v) = ((a * b) * v9)

          .= (a * (b * v9)) by RLVECT_1:def 7

          .= (a * (b * v));

        end;

        then

        reconsider W as RealUnitarySpace by A9, A1, A2, A3, A7, A6, A5, A11, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;

        

         A13: the scalar of W = (the scalar of V || the carrier of W) & the addF of W = (the addF of V || the carrier of W) by RELSET_1: 19;

        ( 0. W) = ( 0. V) & the Mult of W = (the Mult of V | [: REAL , the carrier of W:]) by RELSET_1: 19;

        hence thesis by A13, Def1;

      end;

    end

    begin

    theorem :: RUSUB_1:30

    

     Th30: for V be RealUnitarySpace, W be Subspace of V holds ( (0). W) = ( (0). V)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      the carrier of ( (0). W) = {( 0. W)} & the carrier of ( (0). V) = {( 0. V)} by Def2;

      then

       A1: the carrier of ( (0). W) = the carrier of ( (0). V) by Def1;

      ( (0). W) is Subspace of V by Th21;

      hence thesis by A1, Th24;

    end;

    theorem :: RUSUB_1:31

    

     Th31: for V be RealUnitarySpace, W1,W2 be Subspace of V holds ( (0). W1) = ( (0). W2)

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      ( (0). W1) = ( (0). V) by Th30;

      hence thesis by Th30;

    end;

    theorem :: RUSUB_1:32

    for V be RealUnitarySpace, W be Subspace of V holds ( (0). W) is Subspace of V by Th21;

    theorem :: RUSUB_1:33

    for V be RealUnitarySpace, W be Subspace of V holds ( (0). V) is Subspace of W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      the carrier of ( (0). V) = {( 0. V)} by Def2

      .= {( 0. W)} by Def1;

      hence thesis by Th22;

    end;

    theorem :: RUSUB_1:34

    for V be RealUnitarySpace, W1,W2 be Subspace of V holds ( (0). W1) is Subspace of W2

    proof

      let V be RealUnitarySpace;

      let W1,W2 be Subspace of V;

      ( (0). W1) = ( (0). W2) by Th31;

      hence thesis;

    end;

    theorem :: RUSUB_1:35

    for V be strict RealUnitarySpace holds V is Subspace of ( (Omega). V);

    begin

    definition

      let V be RealUnitarySpace, v be VECTOR of V, W be Subspace of V;

      :: RUSUB_1:def4

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

      coherence

      proof

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

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

        consider X be set such that

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

        X c= the carrier of V by A1;

        then

        reconsider X as Subset of V;

        

         A2: Y c= X

        proof

          let x be object;

          assume x in Y;

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

          hence thesis by A1;

        end;

        X c= Y

        proof

          let x be object;

          assume x in X;

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

          hence thesis;

        end;

        hence thesis by A2, XBOOLE_0:def 10;

      end;

    end

    

     Lm2: for V be RealUnitarySpace, W be Subspace of V holds (( 0. V) + W) = the carrier of W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      set A = { (( 0. V) + u) where u be VECTOR of V : u in W };

      

       A1: the carrier of W c= A

      proof

        let x be object;

        assume x in the carrier of W;

        then

         A2: x in W;

        then x in V by Th2;

        then

        reconsider y = x as Element of V;

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

        hence thesis by A2;

      end;

      A c= the carrier of W

      proof

        let x be object;

        assume x in A;

        then

        consider u be VECTOR of V such that

         A3: x = (( 0. V) + u) and

         A4: u in W;

        x = u by A3, RLVECT_1: 4;

        hence thesis by A4;

      end;

      hence thesis by A1;

    end;

    definition

      let V be RealUnitarySpace;

      let W be Subspace of V;

      :: RUSUB_1:def5

      mode Coset of W -> Subset of V means

      : Def5: ex v be VECTOR of V st it = (v + W);

      existence

      proof

        reconsider VW = the carrier of W as Subset of V by Def1;

        take VW;

        take ( 0. V);

        thus thesis by Lm2;

      end;

    end

    begin

    theorem :: RUSUB_1:36

    

     Th36: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V holds ( 0. V) in (v + W) iff v in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      thus ( 0. V) in (v + W) implies v in W

      proof

        assume ( 0. V) in (v + W);

        then

        consider u be VECTOR of V such that

         A1: ( 0. V) = (v + u) and

         A2: u in W;

        v = ( - u) by A1, RLVECT_1:def 10;

        hence thesis by A2, Th16;

      end;

      assume v in W;

      then

       A3: ( - v) in W by Th16;

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

      .= (v + ( - v));

      hence thesis by A3;

    end;

    theorem :: RUSUB_1:37

    

     Th37: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V holds v in (v + W)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

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

      hence thesis;

    end;

    theorem :: RUSUB_1:38

    for V be RealUnitarySpace, W be Subspace of V holds (( 0. V) + W) = the carrier of W by Lm2;

    theorem :: RUSUB_1:39

    

     Th39: for V be RealUnitarySpace, v be VECTOR of V holds (v + ( (0). V)) = {v}

    proof

      let V be RealUnitarySpace;

      let v be VECTOR of V;

      thus (v + ( (0). V)) c= {v}

      proof

        let x be object;

        assume x in (v + ( (0). V));

        then

        consider u be VECTOR of V such that

         A1: x = (v + u) and

         A2: u in ( (0). V);

        

         A3: the carrier of ( (0). V) = {( 0. V)} by Def2;

        u in the carrier of ( (0). V) by A2;

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

        then x = v by A1, RLVECT_1: 4;

        hence thesis by TARSKI:def 1;

      end;

      let x be object;

      assume x in {v};

      then

       A4: x = v by TARSKI:def 1;

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

      hence thesis by A4;

    end;

    

     Lm3: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V holds v in W iff (v + W) = the carrier of W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

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

      then

       A1: v in { (v + u) where u be VECTOR of V : u in W };

      thus v in W implies (v + W) = the carrier of W

      proof

        assume

         A2: v in W;

        thus (v + W) c= the carrier of W

        proof

          let x be object;

          assume x in (v + W);

          then

          consider u be VECTOR of V such that

           A3: x = (v + u) and

           A4: u in W;

          (v + u) in W by A2, A4, Th14;

          hence thesis by A3;

        end;

        let x be object;

        assume x in the carrier of W;

        then

        reconsider y = x, z = v as Element of W by A2;

        reconsider y1 = y, z1 = z as VECTOR of V by Th3;

        

         A5: (z + (y - z)) = ((y + z) - z) by RLVECT_1:def 3

        .= (y + (z - z)) by RLVECT_1:def 3

        .= (y + ( 0. W)) by RLVECT_1: 15

        .= x by RLVECT_1: 4;

        (y - z) in W;

        then

         A6: (y1 - z1) in W by Th10;

        (y - z) = (y1 - z1) by Th10;

        then (z1 + (y1 - z1)) = x by A5, Th6;

        hence thesis by A6;

      end;

      assume

       A7: (v + W) = the carrier of W;

      assume not v in W;

      hence thesis by A7, A1;

    end;

    theorem :: RUSUB_1:40

    

     Th40: for V be RealUnitarySpace, v be VECTOR of V holds (v + ( (Omega). V)) = the carrier of V by STRUCT_0:def 5, Lm3;

    theorem :: RUSUB_1:41

    

     Th41: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V holds ( 0. V) in (v + W) iff (v + W) = the carrier of W by Th36, Lm3;

    theorem :: RUSUB_1:42

    for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V holds v in W iff (v + W) = the carrier of W by Lm3;

    theorem :: RUSUB_1:43

    

     Th43: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V, a be Real st v in W holds ((a * v) + W) = the carrier of W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      let a be Real;

      assume

       A1: v in W;

      thus ((a * v) + W) c= the carrier of W

      proof

        let x be object;

        assume x in ((a * v) + W);

        then

        consider u be VECTOR of V such that

         A2: x = ((a * v) + u) and

         A3: u in W;

        (a * v) in W by A1, Th15;

        then ((a * v) + u) in W by A3, Th14;

        hence thesis by A2;

      end;

      let x be object;

      assume

       A4: x in the carrier of W;

      then

       A5: x in W;

      the carrier of W c= the carrier of V by Def1;

      then

      reconsider y = x as Element of V by A4;

      

       A6: ((a * v) + (y - (a * v))) = ((y + (a * v)) - (a * v)) by RLVECT_1:def 3

      .= (y + ((a * v) - (a * v))) by RLVECT_1:def 3

      .= (y + ( 0. V)) by RLVECT_1: 15

      .= x by RLVECT_1: 4;

      (a * v) in W by A1, Th15;

      then (y - (a * v)) in W by A5, Th17;

      hence thesis by A6;

    end;

    theorem :: RUSUB_1:44

    

     Th44: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V, a be Real st a <> 0 & ((a * v) + W) = the carrier of W holds v in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      let a be Real;

      assume that

       A1: a <> 0 and

       A2: ((a * v) + W) = the carrier of W;

      assume not v in W;

      then not (1 * v) in W by RLVECT_1:def 8;

      then not (((a " ) * a) * v) in W by A1, XCMPLX_0:def 7;

      then not ((a " ) * (a * v)) in W by RLVECT_1:def 7;

      then

       A3: not (a * v) in W by Th15;

      ( 0. V) in W & ((a * v) + ( 0. V)) = (a * v) by Th11, RLVECT_1: 4;

      then (a * v) in { ((a * v) + u) where u be VECTOR of V : u in W };

      hence contradiction by A2, A3;

    end;

    theorem :: RUSUB_1:45

    

     Th45: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V holds v in W iff (( - v) + W) = the carrier of W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      v in W iff ((( - jj) * v) + W) = the carrier of W by Th43, Th44;

      hence thesis by RLVECT_1: 16;

    end;

    theorem :: RUSUB_1:46

    

     Th46: for V be RealUnitarySpace, W be Subspace of V, u,v be VECTOR of V holds u in W iff (v + W) = ((v + u) + W)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let u,v be VECTOR of V;

      thus u in W implies (v + W) = ((v + u) + W)

      proof

        assume

         A1: u in W;

        thus (v + W) c= ((v + u) + W)

        proof

          let x be object;

          assume x in (v + W);

          then

          consider v1 be VECTOR of V such that

           A2: x = (v + v1) and

           A3: v1 in W;

          

           A4: ((v + u) + (v1 - u)) = (v + (u + (v1 - u))) by RLVECT_1:def 3

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

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

          .= (v + (v1 + ( 0. V))) by RLVECT_1: 15

          .= x by A2, RLVECT_1: 4;

          (v1 - u) in W by A1, A3, Th17;

          hence thesis by A4;

        end;

        let x be object;

        assume x in ((v + u) + W);

        then

        consider v2 be VECTOR of V such that

         A5: x = ((v + u) + v2) and

         A6: v2 in W;

        

         A7: x = (v + (u + v2)) by A5, RLVECT_1:def 3;

        (u + v2) in W by A1, A6, Th14;

        hence thesis by A7;

      end;

      assume

       A8: (v + W) = ((v + u) + W);

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

      then v in ((v + u) + W) by A8;

      then

      consider u1 be VECTOR of V such that

       A9: v = ((v + u) + u1) and

       A10: u1 in W;

      v = (v + ( 0. V)) & v = (v + (u + u1)) by A9, RLVECT_1: 4, RLVECT_1:def 3;

      then (u + u1) = ( 0. V) by RLVECT_1: 8;

      then u = ( - u1) by RLVECT_1:def 10;

      hence thesis by A10, Th16;

    end;

    theorem :: RUSUB_1:47

    for V be RealUnitarySpace, W be Subspace of V, u,v be VECTOR of V holds u in W iff (v + W) = ((v - u) + W)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let u,v be VECTOR of V;

      

       A1: ( - u) in W implies u in W

      proof

        assume ( - u) in W;

        then ( - ( - u)) in W by Th16;

        hence thesis by RLVECT_1: 17;

      end;

      ( - u) in W iff (v + W) = ((v + ( - u)) + W) by Th46;

      hence thesis by A1, Th16;

    end;

    theorem :: RUSUB_1:48

    

     Th48: for V be RealUnitarySpace, W be Subspace of V, u,v be VECTOR of V holds v in (u + W) iff (u + W) = (v + W)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let u,v be VECTOR of V;

      thus v in (u + W) implies (u + W) = (v + W)

      proof

        assume v in (u + W);

        then

        consider z be VECTOR of V such that

         A1: v = (u + z) and

         A2: z in W;

        thus (u + W) c= (v + W)

        proof

          let x be object;

          assume x in (u + W);

          then

          consider v1 be VECTOR of V such that

           A3: x = (u + v1) and

           A4: v1 in W;

          (v - z) = (u + (z - z)) by A1, RLVECT_1:def 3

          .= (u + ( 0. V)) by RLVECT_1: 15

          .= u by RLVECT_1: 4;

          

          then

           A5: x = (v + (v1 + ( - z))) by A3, RLVECT_1:def 3

          .= (v + (v1 - z));

          (v1 - z) in W by A2, A4, Th17;

          hence thesis by A5;

        end;

        let x be object;

        assume x in (v + W);

        then

        consider v2 be VECTOR of V such that

         A6: x = (v + v2) & v2 in W;

        (z + v2) in W & x = (u + (z + v2)) by A1, A2, A6, Th14, RLVECT_1:def 3;

        hence thesis;

      end;

      thus thesis by Th37;

    end;

    theorem :: RUSUB_1:49

    

     Th49: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V holds (v + W) = (( - v) + W) iff v in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      thus (v + W) = (( - v) + W) implies v in W

      proof

        assume (v + W) = (( - v) + W);

        then v in (( - v) + W) by Th37;

        then

        consider u be VECTOR of V such that

         A1: v = (( - v) + u) and

         A2: u in W;

        ( 0. V) = (v - (( - v) + u)) by A1, RLVECT_1: 15

        .= ((v - ( - v)) - u) by RLVECT_1: 27

        .= ((v + v) - u) by RLVECT_1: 17

        .= (((1 * v) + v) - u) by RLVECT_1:def 8

        .= (((1 * v) + (1 * v)) - u) by RLVECT_1:def 8

        .= (((1 + 1) * v) - u) by RLVECT_1:def 6

        .= ((2 * v) - u);

        then ((2 " ) * (2 * v)) = ((2 " ) * u) by RLVECT_1: 21;

        then (((2 " ) * 2) * v) = ((2 " ) * u) by RLVECT_1:def 7;

        then v = ((2 " ) * u) by RLVECT_1:def 8;

        hence thesis by A2, Th15;

      end;

      assume

       A3: v in W;

      then (v + W) = the carrier of W by Lm3;

      hence thesis by A3, Th45;

    end;

    theorem :: RUSUB_1:50

    

     Th50: for V be RealUnitarySpace, W be Subspace of V, u,v1,v2 be VECTOR of V st u in (v1 + W) & u in (v2 + W) holds (v1 + W) = (v2 + W)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let u,v1,v2 be VECTOR of V;

      assume that

       A1: u in (v1 + W) and

       A2: u in (v2 + W);

      consider x1 be VECTOR of V such that

       A3: u = (v1 + x1) and

       A4: x1 in W by A1;

      consider x2 be VECTOR of V such that

       A5: u = (v2 + x2) and

       A6: x2 in W by A2;

      thus (v1 + W) c= (v2 + W)

      proof

        let x be object;

        assume x in (v1 + W);

        then

        consider u1 be VECTOR of V such that

         A7: x = (v1 + u1) and

         A8: u1 in W;

        (x2 - x1) in W by A4, A6, Th17;

        then

         A9: ((x2 - x1) + u1) in W by A8, Th14;

        (u - x1) = (v1 + (x1 - x1)) by A3, RLVECT_1:def 3

        .= (v1 + ( 0. V)) by RLVECT_1: 15

        .= v1 by RLVECT_1: 4;

        

        then x = ((v2 + (x2 - x1)) + u1) by A5, A7, RLVECT_1:def 3

        .= (v2 + ((x2 - x1) + u1)) by RLVECT_1:def 3;

        hence thesis by A9;

      end;

      let x be object;

      assume x in (v2 + W);

      then

      consider u1 be VECTOR of V such that

       A10: x = (v2 + u1) and

       A11: u1 in W;

      (x1 - x2) in W by A4, A6, Th17;

      then

       A12: ((x1 - x2) + u1) in W by A11, Th14;

      (u - x2) = (v2 + (x2 - x2)) by A5, RLVECT_1:def 3

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

      .= v2 by RLVECT_1: 4;

      

      then x = ((v1 + (x1 - x2)) + u1) by A3, A10, RLVECT_1:def 3

      .= (v1 + ((x1 - x2) + u1)) by RLVECT_1:def 3;

      hence thesis by A12;

    end;

    theorem :: RUSUB_1:51

    for V be RealUnitarySpace, W be Subspace of V, u,v be VECTOR of V st u in (v + W) & u in (( - v) + W) holds v in W by Th50, Th49;

    theorem :: RUSUB_1:52

    

     Th52: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V, a be Real st a <> 1 & (a * v) in (v + W) holds v in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      let a be Real;

      assume that

       A1: a <> 1 and

       A2: (a * v) in (v + W);

      

       A3: (a - 1) <> 0 by A1;

      consider u be VECTOR of V such that

       A4: (a * v) = (v + u) and

       A5: u in W by A2;

      u = (u + ( 0. V)) by RLVECT_1: 4

      .= (u + (v - v)) by RLVECT_1: 15

      .= ((a * v) - v) by A4, RLVECT_1:def 3

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

      .= ((a - 1) * v) by RLVECT_1: 35;

      then (((a - 1) " ) * u) = ((((a - 1) " ) * (a - 1)) * v) by RLVECT_1:def 7;

      then (1 * v) = (((a - 1) " ) * u) by A3, XCMPLX_0:def 7;

      then v = (((a - 1) " ) * u) by RLVECT_1:def 8;

      hence thesis by A5, Th15;

    end;

    theorem :: RUSUB_1:53

    

     Th53: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V, a be Real st v in W holds (a * v) in (v + W)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      let a be Real;

      assume v in W;

      then

       A1: ((a - 1) * v) in W by Th15;

      (a * v) = (((a - 1) + 1) * v)

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

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

      hence thesis by A1;

    end;

    theorem :: RUSUB_1:54

    for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V holds ( - v) in (v + W) iff v in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      (( - jj) * v) = ( - v) by RLVECT_1: 16;

      hence thesis by Th52, Th53;

    end;

    theorem :: RUSUB_1:55

    

     Th55: for V be RealUnitarySpace, W be Subspace of V, u,v be VECTOR of V holds (u + v) in (v + W) iff u in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let u,v be VECTOR of V;

      thus (u + v) in (v + W) implies u in W

      proof

        assume (u + v) in (v + W);

        then ex v1 be VECTOR of V st (u + v) = (v + v1) & v1 in W;

        hence thesis by RLVECT_1: 8;

      end;

      assume u in W;

      hence thesis;

    end;

    theorem :: RUSUB_1:56

    for V be RealUnitarySpace, W be Subspace of V, u,v be VECTOR of V holds (v - u) in (v + W) iff u in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let u,v be VECTOR of V;

      

       A1: (v - u) = (( - u) + v);

      

       A2: ( - u) in W implies ( - ( - u)) in W by Th16;

      u in W implies ( - u) in W by Th16;

      hence thesis by A1, A2, Th55, RLVECT_1: 17;

    end;

    theorem :: RUSUB_1:57

    

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

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let u,v be VECTOR of V;

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

      proof

        assume u in (v + W);

        then ex v1 be VECTOR of V st u = (v + v1) & v1 in W;

        hence thesis;

      end;

      given v1 be VECTOR of V such that

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

      thus thesis by A1;

    end;

    theorem :: RUSUB_1:58

    for V be RealUnitarySpace, W be Subspace of V, u,v be VECTOR of V holds u in (v + W) iff ex v1 be VECTOR of V st v1 in W & u = (v - v1)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let u,v be VECTOR of V;

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

      proof

        assume u in (v + W);

        then

        consider v1 be VECTOR of V such that

         A1: u = (v + v1) and

         A2: v1 in W;

        take x = ( - v1);

        thus x in W by A2, Th16;

        thus thesis by A1, RLVECT_1: 17;

      end;

      given v1 be VECTOR of V such that

       A3: v1 in W and

       A4: u = (v - v1);

      ( - v1) in W by A3, Th16;

      hence thesis by A4;

    end;

    theorem :: RUSUB_1:59

    

     Th59: for V be RealUnitarySpace, W be Subspace of V, v1,v2 be VECTOR of V holds (ex v be VECTOR of V st v1 in (v + W) & v2 in (v + W)) iff (v1 - v2) in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v1,v2 be VECTOR of V;

      thus (ex v be VECTOR of V st v1 in (v + W) & v2 in (v + W)) implies (v1 - v2) in W

      proof

        given v be VECTOR of V such that

         A1: v1 in (v + W) and

         A2: v2 in (v + W);

        consider u2 be VECTOR of V such that

         A3: u2 in W and

         A4: v2 = (v + u2) by A2, Th57;

        consider u1 be VECTOR of V such that

         A5: u1 in W and

         A6: v1 = (v + u1) by A1, Th57;

        (v1 - v2) = ((u1 + v) + (( - v) - u2)) by A6, A4, RLVECT_1: 30

        .= (((u1 + v) + ( - v)) - u2) by RLVECT_1:def 3

        .= ((u1 + (v + ( - v))) - u2) by RLVECT_1:def 3

        .= ((u1 + ( 0. V)) - u2) by RLVECT_1: 5

        .= (u1 - u2) by RLVECT_1: 4;

        hence thesis by A5, A3, Th17;

      end;

      assume (v1 - v2) in W;

      then

       A7: ( - (v1 - v2)) in W by Th16;

      take v1;

      thus v1 in (v1 + W) by Th37;

      (v1 + ( - (v1 - v2))) = (v1 + (( - v1) + v2)) by RLVECT_1: 33

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

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

      .= v2 by RLVECT_1: 4;

      hence thesis by A7;

    end;

    theorem :: RUSUB_1:60

    

     Th60: for V be RealUnitarySpace, W be Subspace of V, u,v be VECTOR of V st (v + W) = (u + W) holds ex v1 be VECTOR of V st v1 in W & (v + v1) = u

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let u,v be VECTOR of V;

      assume (v + W) = (u + W);

      then v in (u + W) by Th37;

      then

      consider u1 be VECTOR of V such that

       A1: v = (u + u1) and

       A2: u1 in W;

      take v1 = (u - v);

      ( 0. V) = ((u + u1) - v) by A1, RLVECT_1: 15

      .= (u1 + (u - v)) by RLVECT_1:def 3;

      then v1 = ( - u1) by RLVECT_1:def 10;

      hence v1 in W by A2, Th16;

      

      thus (v + v1) = ((u + v) - v) by RLVECT_1:def 3

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

      .= (u + ( 0. V)) by RLVECT_1: 15

      .= u by RLVECT_1: 4;

    end;

    theorem :: RUSUB_1:61

    

     Th61: for V be RealUnitarySpace, W be Subspace of V, u,v be VECTOR of V st (v + W) = (u + W) holds ex v1 be VECTOR of V st v1 in W & (v - v1) = u

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let u,v be VECTOR of V;

      assume (v + W) = (u + W);

      then u in (v + W) by Th37;

      then

      consider u1 be VECTOR of V such that

       A1: u = (v + u1) and

       A2: u1 in W;

      take v1 = (v - u);

      ( 0. V) = ((v + u1) - u) by A1, RLVECT_1: 15

      .= (u1 + (v - u)) by RLVECT_1:def 3;

      then v1 = ( - u1) by RLVECT_1:def 10;

      hence v1 in W by A2, Th16;

      

      thus (v - v1) = ((v - v) + u) by RLVECT_1: 29

      .= (( 0. V) + u) by RLVECT_1: 15

      .= u by RLVECT_1: 4;

    end;

    theorem :: RUSUB_1:62

    

     Th62: for V be RealUnitarySpace, W1,W2 be strict Subspace of V, v be VECTOR of V holds (v + W1) = (v + W2) iff W1 = W2

    proof

      let V be RealUnitarySpace;

      let W1,W2 be strict Subspace of V;

      let v be VECTOR of V;

      thus (v + W1) = (v + W2) implies W1 = W2

      proof

        assume

         A1: (v + W1) = (v + W2);

        the carrier of W1 = the carrier of W2

        proof

          

           A2: the carrier of W1 c= the carrier of V by Def1;

          thus the carrier of W1 c= the carrier of W2

          proof

            let x be object;

            assume

             A3: x in the carrier of W1;

            then

            reconsider y = x as Element of V by A2;

            set z = (v + y);

            x in W1 by A3;

            then z in (v + W2) by A1;

            then

            consider u be VECTOR of V such that

             A4: z = (v + u) and

             A5: u in W2;

            y = u by A4, RLVECT_1: 8;

            hence thesis by A5;

          end;

          let x be object;

          assume

           A6: x in the carrier of W2;

          the carrier of W2 c= the carrier of V by Def1;

          then

          reconsider y = x as Element of V by A6;

          set z = (v + y);

          x in W2 by A6;

          then z in (v + W1) by A1;

          then

          consider u be VECTOR of V such that

           A7: z = (v + u) and

           A8: u in W1;

          y = u by A7, RLVECT_1: 8;

          hence thesis by A8;

        end;

        hence thesis by Th24;

      end;

      thus thesis;

    end;

    theorem :: RUSUB_1:63

    

     Th63: for V be RealUnitarySpace, W1,W2 be strict Subspace of V, u,v be VECTOR of V st (v + W1) = (u + W2) holds W1 = W2

    proof

      let V be RealUnitarySpace;

      let W1,W2 be strict Subspace of V;

      let u,v be VECTOR of V;

      assume

       A1: (v + W1) = (u + W2);

      set V2 = the carrier of W2;

      set V1 = the carrier of W1;

      assume

       A2: W1 <> W2;

       A3:

      now

        set x = the Element of (V1 \ V2);

        assume (V1 \ V2) <> {} ;

        then x in V1 by XBOOLE_0:def 5;

        then

         A4: x in W1;

        then x in V by Th2;

        then

        reconsider x as Element of V;

        set z = (v + x);

        z in (u + W2) by A1, A4;

        then

        consider u1 be VECTOR of V such that

         A5: z = (u + u1) and

         A6: u1 in W2;

        x = (( 0. V) + x) by RLVECT_1: 4

        .= ((v - v) + x) by RLVECT_1: 15

        .= (( - v) + (u + u1)) by A5, RLVECT_1:def 3;

        then

         A7: ((v + (( - v) + (u + u1))) + W1) = (v + W1) by A4, Th46;

        (v + (( - v) + (u + u1))) = ((v - v) + (u + u1)) by RLVECT_1:def 3

        .= (( 0. V) + (u + u1)) by RLVECT_1: 15

        .= (u + u1) by RLVECT_1: 4;

        then ((u + u1) + W2) = ((u + u1) + W1) by A1, A6, A7, Th46;

        hence thesis by A2, Th62;

      end;

       A8:

      now

        set x = the Element of (V2 \ V1);

        assume (V2 \ V1) <> {} ;

        then x in V2 by XBOOLE_0:def 5;

        then

         A9: x in W2;

        then x in V by Th2;

        then

        reconsider x as Element of V;

        set z = (u + x);

        z in (v + W1) by A1, A9;

        then

        consider u1 be VECTOR of V such that

         A10: z = (v + u1) and

         A11: u1 in W1;

        x = (( 0. V) + x) by RLVECT_1: 4

        .= ((u - u) + x) by RLVECT_1: 15

        .= (( - u) + (v + u1)) by A10, RLVECT_1:def 3;

        then

         A12: ((u + (( - u) + (v + u1))) + W2) = (u + W2) by A9, Th46;

        (u + (( - u) + (v + u1))) = ((u - u) + (v + u1)) by RLVECT_1:def 3

        .= (( 0. V) + (v + u1)) by RLVECT_1: 15

        .= (v + u1) by RLVECT_1: 4;

        then ((v + u1) + W1) = ((v + u1) + W2) by A1, A11, A12, Th46;

        hence thesis by A2, Th62;

      end;

      V1 <> V2 by A2, Th24;

      then not V1 c= V2 or not V2 c= V1;

      hence thesis by A3, A8, XBOOLE_1: 37;

    end;

    theorem :: RUSUB_1:64

    for V be RealUnitarySpace, W be Subspace of V, C be Coset of W holds C is linearly-closed iff C = the carrier of W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let C be Coset of W;

      thus C is linearly-closed implies C = the carrier of W

      proof

        assume

         A1: C is linearly-closed;

        consider v be VECTOR of V such that

         A2: C = (v + W) by Def5;

        C <> {} by A2, Th37;

        then ( 0. V) in (v + W) by A1, A2, RLSUB_1: 1;

        hence thesis by A2, Th41;

      end;

      thus thesis by Lm1;

    end;

    theorem :: RUSUB_1:65

    for V be RealUnitarySpace, W1,W2 be strict Subspace of V, C1 be Coset of W1, C2 be Coset of W2 holds C1 = C2 implies W1 = W2

    proof

      let V be RealUnitarySpace;

      let W1,W2 be strict Subspace of V;

      let C1 be Coset of W1;

      let C2 be Coset of W2;

      (ex v1 be VECTOR of V st C1 = (v1 + W1)) & ex v2 be VECTOR of V st C2 = (v2 + W2) by Def5;

      hence thesis by Th63;

    end;

    theorem :: RUSUB_1:66

    for V be RealUnitarySpace, v be VECTOR of V holds {v} is Coset of ( (0). V)

    proof

      let V be RealUnitarySpace;

      let v be VECTOR of V;

      (v + ( (0). V)) = {v} by Th39;

      hence thesis by Def5;

    end;

    theorem :: RUSUB_1:67

    for V be RealUnitarySpace, V1 be Subset of V holds V1 is Coset of ( (0). V) implies ex v be VECTOR of V st V1 = {v}

    proof

      let V be RealUnitarySpace;

      let V1 be Subset of V;

      assume V1 is Coset of ( (0). V);

      then

      consider v be VECTOR of V such that

       A1: V1 = (v + ( (0). V)) by Def5;

      take v;

      thus thesis by A1, Th39;

    end;

    theorem :: RUSUB_1:68

    for V be RealUnitarySpace, W be Subspace of V holds the carrier of W is Coset of W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      the carrier of W = (( 0. V) + W) by Lm2;

      hence thesis by Def5;

    end;

    theorem :: RUSUB_1:69

    for V be RealUnitarySpace holds the carrier of V is Coset of ( (Omega). V)

    proof

      let V be RealUnitarySpace;

      set v = the VECTOR of V;

      the carrier of V is Subset of V iff the carrier of V c= the carrier of V;

      then

      reconsider A = the carrier of V as Subset of V;

      A = (v + ( (Omega). V)) by Th40;

      hence thesis by Def5;

    end;

    theorem :: RUSUB_1:70

    for V be RealUnitarySpace, V1 be Subset of V st V1 is Coset of ( (Omega). V) holds V1 = the carrier of V

    proof

      let V be RealUnitarySpace;

      let V1 be Subset of V;

      assume V1 is Coset of ( (Omega). V);

      then ex v be VECTOR of V st V1 = (v + ( (Omega). V)) by Def5;

      hence thesis by Th40;

    end;

    theorem :: RUSUB_1:71

    for V be RealUnitarySpace, W be Subspace of V, C be Coset of W holds ( 0. V) in C iff C = the carrier of W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let C be Coset of W;

      ex v be VECTOR of V st C = (v + W) by Def5;

      hence thesis by Th41;

    end;

    theorem :: RUSUB_1:72

    

     Th72: for V be RealUnitarySpace, W be Subspace of V, C be Coset of W, u be VECTOR of V holds u in C iff C = (u + W)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let C be Coset of W;

      let u be VECTOR of V;

      thus u in C implies C = (u + W)

      proof

        assume

         A1: u in C;

        ex v be VECTOR of V st C = (v + W) by Def5;

        hence thesis by A1, Th48;

      end;

      thus thesis by Th37;

    end;

    theorem :: RUSUB_1:73

    for V be RealUnitarySpace, W be Subspace of V, C be Coset of W, u,v be VECTOR of V st u in C & v in C holds ex v1 be VECTOR of V st v1 in W & (u + v1) = v

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let C be Coset of W;

      let u,v be VECTOR of V;

      assume u in C & v in C;

      then C = (u + W) & C = (v + W) by Th72;

      hence thesis by Th60;

    end;

    theorem :: RUSUB_1:74

    for V be RealUnitarySpace, W be Subspace of V, C be Coset of W, u,v be VECTOR of V st u in C & v in C holds ex v1 be VECTOR of V st v1 in W & (u - v1) = v

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let C be Coset of W;

      let u,v be VECTOR of V;

      assume u in C & v in C;

      then C = (u + W) & C = (v + W) by Th72;

      hence thesis by Th61;

    end;

    theorem :: RUSUB_1:75

    for V be RealUnitarySpace, W be Subspace of V, v1,v2 be VECTOR of V holds (ex C be Coset of W st v1 in C & v2 in C) iff (v1 - v2) in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v1,v2 be VECTOR of V;

      thus (ex C be Coset of W st v1 in C & v2 in C) implies (v1 - v2) in W

      proof

        given C be Coset of W such that

         A1: v1 in C & v2 in C;

        ex v be VECTOR of V st C = (v + W) by Def5;

        hence thesis by A1, Th59;

      end;

      assume (v1 - v2) in W;

      then

      consider v be VECTOR of V such that

       A2: v1 in (v + W) & v2 in (v + W) by Th59;

      reconsider C = (v + W) as Coset of W by Def5;

      take C;

      thus thesis by A2;

    end;

    theorem :: RUSUB_1:76

    for V be RealUnitarySpace, W be Subspace of V, u be VECTOR of V, B,C be Coset of W st u in B & u in C holds B = C

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let u be VECTOR of V;

      let B,C be Coset of W;

      assume

       A1: u in B & u in C;

      (ex v1 be VECTOR of V st B = (v1 + W)) & ex v2 be VECTOR of V st C = (v2 + W) by Def5;

      hence thesis by A1, Th50;

    end;