rlsub_1.miz

    begin

    reserve V,X,Y for RealLinearSpace;

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

    reserve a for Real;

    reserve V1,V2,V3 for Subset of V;

    reserve x for object;

    definition

      let V;

      let V1;

      :: RLSUB_1:def1

      attr V1 is linearly-closed means (for v, u st v in V1 & u in V1 holds (v + u) in V1) & for a, v st v in V1 holds (a * v) in V1;

    end

    theorem :: RLSUB_1:1



     Th1: V1 <> {} & V1 is linearly-closed implies ( 0. V) in V1

    proof

      assume that

       A1: V1 <> {} and

       A2: V1 is linearly-closed;

      set x = the Element of V1;

      reconsider x as Element of V by A1, TARSKI:def 3;

      ( 0 * x) in V1 by A1, A2;

      hence thesis by RLVECT_1: 10;

    end;

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

    theorem :: RLSUB_1:2



     Th2: V1 is linearly-closed implies for v st v in V1 holds ( - v) in V1

    proof

      assume

       A1: V1 is linearly-closed;

      let v;

      assume v in V1;

      then (( - jj) * v) in V1 by A1;

      hence thesis by RLVECT_1: 16;

    end;

    theorem :: RLSUB_1:3

    V1 is linearly-closed implies for v, u st v in V1 & u in V1 holds (v - u) in V1

    proof

      assume

       A1: V1 is linearly-closed;

      let v, u;

      assume that

       A2: v in V1 and

       A3: u in V1;

      ( - u) in V1 by A1, A3, Th2;

      hence thesis by A1, A2;

    end;

    theorem :: RLSUB_1:4



     Th4: {( 0. V)} is linearly-closed

    proof

      thus for v, u st v in {( 0. V)} & u in {( 0. V)} holds (v + u) in {( 0. V)}

      proof

        let v, u;

        assume v in {( 0. V)} & u in {( 0. V)};

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

        then (v + u) = ( 0. V);

        hence thesis by TARSKI:def 1;

      end;

      let a, v;

      assume

       A1: v in {( 0. V)};

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

      hence thesis by A1;

    end;

    theorem :: RLSUB_1:5

    the carrier of V = V1 implies V1 is linearly-closed;

    theorem :: RLSUB_1:6

    V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) : v in V1 & u in V2 } implies V3 is linearly-closed

    proof

      assume that

       A1: V1 is linearly-closed & V2 is linearly-closed and

       A2: V3 = { (v + u) : v in V1 & u in V2 };

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

      proof

        let v, u;

        assume that

         A3: v in V3 and

         A4: u in V3;

        consider v2, v1 such that

         A5: v = (v1 + v2) and

         A6: v1 in V1 & v2 in V2 by A2, A3;

        consider u2, u1 such that

         A7: u = (u1 + u2) and

         A8: u1 in V1 & u2 in V2 by A2, A4;



         A9: (v + u) = (((v1 + v2) + u1) + u2) by A5, A7, RLVECT_1:def 3

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

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

        (v1 + u1) in V1 & (v2 + u2) in V2 by A1, A6, A8;

        hence thesis by A2, A9;

      end;

      let a, v;

      assume v in V3;

      then

      consider v2, v1 such that

       A10: v = (v1 + v2) and

       A11: v1 in V1 & v2 in V2 by A2;



       A12: (a * v) = ((a * v1) + (a * v2)) by A10, RLVECT_1:def 5;

      (a * v1) in V1 & (a * v2) in V2 by A1, A11;

      hence thesis by A2, A12;

    end;

    theorem :: RLSUB_1:7

    V1 is linearly-closed & V2 is linearly-closed implies (V1 /\ V2) is linearly-closed

    proof

      assume that

       A1: V1 is linearly-closed and

       A2: V2 is linearly-closed;

      thus for v, u st v in (V1 /\ V2) & u in (V1 /\ V2) holds (v + u) in (V1 /\ V2)

      proof

        let v, u;

        assume

         A3: v in (V1 /\ V2) & u in (V1 /\ V2);

        then v in V2 & u in V2 by XBOOLE_0:def 4;

        then

         A4: (v + u) in V2 by A2;

        v in V1 & u in V1 by A3, XBOOLE_0:def 4;

        then (v + u) in V1 by A1;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      let a, v;

      assume

       A5: v in (V1 /\ V2);

      then v in V2 by XBOOLE_0:def 4;

      then

       A6: (a * v) in V2 by A2;

      v in V1 by A5, XBOOLE_0:def 4;

      then (a * v) in V1 by A1;

      hence thesis by A6, XBOOLE_0:def 4;

    end;

    definition

      let V;

      :: RLSUB_1:def2

      mode Subspace of V -> RealLinearSpace means

      : Def2: 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 :]);

      existence

      proof

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

        hence thesis;

      end;

    end

    reserve W,W1,W2 for Subspace of V;

    reserve w,w1,w2 for VECTOR of W;

    theorem :: RLSUB_1:8

    x in W1 & W1 is Subspace of W2 implies x in W2

    proof

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

      hence thesis;

    end;

    theorem :: RLSUB_1:9



     Th9: x in W implies x in V

    proof

      assume x in W;

      then

       A1: x in the carrier of W;

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

      hence thesis by A1;

    end;

    theorem :: RLSUB_1:10



     Th10: w is VECTOR of V

    proof

      w in V by Th9, RLVECT_1: 1;

      hence thesis;

    end;

    theorem :: RLSUB_1:11

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

    theorem :: RLSUB_1:12

    ( 0. W1) = ( 0. W2)

    proof



      thus ( 0. W1) = ( 0. V) by Def2

      .= ( 0. W2) by Def2;

    end;

    theorem :: RLSUB_1:13



     Th13: w1 = v & w2 = u implies (w1 + w2) = (v + u)

    proof

      assume

       A1: v = w1 & u = w2;

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

      hence thesis by A1, FUNCT_1: 49;

    end;

    theorem :: RLSUB_1:14



     Th14: w = v implies (a * w) = (a * v)

    proof

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

      then (aa * w) = (aa * v) by A1, FUNCT_1: 49;

      hence thesis;

    end;

    theorem :: RLSUB_1:15



     Th15: w = v implies ( - v) = ( - w)

    proof



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

      assume w = v;

      hence thesis by A1, Th14;

    end;

    theorem :: RLSUB_1:16



     Th16: w1 = v & w2 = u implies (w1 - w2) = (v - u)

    proof

      assume that

       A1: w1 = v and

       A2: w2 = u;

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

      hence thesis by A1, Th13;

    end;



     Lm1: the carrier of W = V1 implies V1 is linearly-closed

    proof

      set VW = the carrier of W;

      reconsider WW = W as RealLinearSpace;

      assume

       A1: the carrier of W = V1;

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

      proof

        let v, u;

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

      end;

      let a, 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 Th14;

    end;

    theorem :: RLSUB_1:17



     Th17: ( 0. V) in W

    proof

      ( 0. W) in W;

      hence thesis by Def2;

    end;

    theorem :: RLSUB_1:18

    ( 0. W1) in W2

    proof

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

      hence thesis by Th17;

    end;

    theorem :: RLSUB_1:19

    ( 0. W) in V by Th9, RLVECT_1: 1;

    theorem :: RLSUB_1:20



     Th20: u in W & v in W implies (u + v) in W

    proof

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

      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;

      hence thesis;

    end;

    theorem :: RLSUB_1:21



     Th21: v in W implies (a * v) in W

    proof

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

      assume v in W;

      then

       A1: v in the carrier of W;

      VW is linearly-closed by Lm1;

      then (a * v) in the carrier of W by A1;

      hence thesis;

    end;

    theorem :: RLSUB_1:22



     Th22: v in W implies ( - v) in W

    proof

      assume v in W;

      then (( - jj) * v) in W by Th21;

      hence thesis by RLVECT_1: 16;

    end;

    theorem :: RLSUB_1:23



     Th23: u in W & v in W implies (u - v) in W

    proof

      assume that

       A1: u in W and

       A2: v in W;

      ( - v) in W by A2, Th22;

      hence thesis by A1, Th20;

    end;

    reserve D for non empty set;

    reserve d1 for Element of D;

    reserve A for BinOp of D;

    reserve M for Function of [: REAL , D:], D;

    theorem :: RLSUB_1:24



     Th24: V1 = D & d1 = ( 0. V) & A = (the addF of V || V1) & M = (the Mult of V | [: REAL , V1:]) implies RLSStruct (# D, d1, A, M #) is Subspace of V

    proof

      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:]);

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



       A5: for a holds for x be VECTOR of W holds (a * x) = (the Mult of V . (a,x))

      proof

        let a;

        let x be VECTOR of W;

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



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

        .= (the Mult of V . (a,x));

      end;



       A6: for x,y be VECTOR of W holds (x + y) = (the addF of V . (x,y))

      proof

        let x,y be VECTOR of W;



        thus (x + y) = (the addF of V . [x, y]) by A1, A3, FUNCT_1: 49

        .= (the addF of V . (x,y));

      end;



       A7: W is Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital

      proof

        set MV = the Mult of V;

        set AV = the addF of V;

        thus W is Abelian

        proof

          let x,y be VECTOR of W;

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



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

          .= (y1 + x1)

          .= (y + x) by A6;

        end;

        thus W is add-associative

        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 A6

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

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

          .= (AV . (x1,(y + z))) by A6

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

        end;

        thus W is right_zeroed

        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, A6

          .= x;

        end;

        thus 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 such that

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

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

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

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

          then

          reconsider y = v as VECTOR of W;

          take y;

          thus thesis by A2, A6, A8;

        end;

        thus for a be Real holds for 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 Real;

          (a * (x + y)) = (MV . (a,(x + y))) by A5

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

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

          .= (AV . ((MV . (a,x1)),(a * y))) by A5

          .= (AV . ((a * x),(a * y))) by A5

          .= ((a * x) + (a * y)) by A6;

          hence thesis;

        end;

        thus for a,b be Real holds for 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 A5

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

          .= (AV . ((MV . (a,y)),(b * x))) by A5

          .= (AV . ((a * x),(b * x))) by A5

          .= ((a * x) + (b * x)) by A6;

          hence thesis;

        end;

        thus for a,b be Real holds for 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 Real;

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

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

          .= (MV . (a,(b * x))) by A5

          .= (a * (b * x)) by A5;

          hence thesis;

        end;

        let x be VECTOR of W;

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



        thus (1 * x) = (jj * y) by A5

        .= x by RLVECT_1:def 8;

      end;

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

      hence thesis by A1, A3, A4, A7, Def2;

    end;

    theorem :: RLSUB_1:25



     Th25: V is Subspace of V

    proof

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

      thus thesis by RELSET_1: 19;

    end;

    theorem :: RLSUB_1:26



     Th26: for V,X be strict RealLinearSpace holds V is Subspace of X & X is Subspace of V implies V = X

    proof

      let V,X be strict RealLinearSpace;

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

      then

       A3: VV = VX;

      set AX = the addF of X;

      set AV = the addF of V;

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

      then

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

      set MX = the Mult of X;

      set MV = the Mult of V;



       A5: MX = (MV | [: REAL , VX:]) by A2, Def2;

      ( 0. V) = ( 0. X) & MV = (MX | [: REAL , VV:]) by A1, Def2;

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

    end;

    theorem :: RLSUB_1:27



     Th27: V is Subspace of X & X is Subspace of Y implies V is Subspace of Y

    proof

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

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

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

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

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

        then

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

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

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

        hence thesis by A3, FUNCT_1: 51;

      end;

      set MY = the Mult of Y;

      set MX = the Mult of X;

      set MV = the Mult of V;

      set VX = the carrier of X;

      set VV = the carrier of V;

      VV c= VX by A1, Def2;

      then

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

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

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

      hence thesis by A4, FUNCT_1: 51;

    end;

    theorem :: RLSUB_1:28



     Th28: the carrier of W1 c= the carrier of W2 implies W1 is Subspace of W2

    proof

      set VW1 = the carrier of W1;

      set VW2 = the carrier of W2;

      set AV = the addF of V;

      set MV = the Mult 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 Def2;

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

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

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

      hence thesis by A3, FUNCT_1: 51;

    end;

    theorem :: RLSUB_1:29

    (for v st v in W1 holds v in W2) implies W1 is Subspace of W2

    proof

      assume

       A1: for 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 Def2;

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

    end;

    registration

      let V;

      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;

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

        then RLSStruct (# the carrier of V, ( 0. V), the addF of V, the Mult of V #) is Subspace of V by Th24;

        hence thesis;

      end;

    end

    theorem :: RLSUB_1:30



     Th30: for W1,W2 be strict Subspace of V holds the carrier of W1 = the carrier of W2 implies W1 = W2

    proof

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

      hence thesis by Th26;

    end;

    theorem :: RLSUB_1:31



     Th31: for W1,W2 be strict Subspace of V holds (for v holds v in W1 iff v in W2) implies W1 = W2

    proof

      let W1,W2 be strict Subspace of V;

      assume

       A1: for 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 Def2;

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

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

    end;

    theorem :: RLSUB_1:32

    for V be strict RealLinearSpace, W be strict Subspace of V holds the carrier of W = the carrier of V implies W = V

    proof

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

      assume

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

      V is Subspace of V by Th25;

      hence thesis by A1, Th30;

    end;

    theorem :: RLSUB_1:33

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

    proof

      let V be strict RealLinearSpace, 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 Th25;

      hence thesis by A1, Th31;

    end;

    theorem :: RLSUB_1:34

    the carrier of W = V1 implies V1 is linearly-closed by Lm1;

    theorem :: RLSUB_1:35



     Th35: V1 <> {} & V1 is linearly-closed implies ex W be strict Subspace of V st V1 = the carrier of W

    proof

      assume that

       A1: V1 <> {} and

       A2: V1 is linearly-closed;

      reconsider D = V1 as non empty set by A1;

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

      set VV = the carrier of V;

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

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

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

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

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

      then

       A12: ( dom A) = [:D, D:] by 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

           A13: y in D;

          then

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



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



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

          .= y;

          hence thesis by A12, A14;

        end;

        given x be object such that

         A15: x in ( dom A) and

         A16: y = (A . x);

        consider x1,x2 be object such that

         A17: x1 in D & x2 in D and

         A18: x = [x1, x2] by A12, A15, ZFMISC_1:def 2;

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

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

        then y = (v1 + v2) by A16, A18, FUNCT_1: 49;

        hence y in D by A2, A17;

      end;

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

      then

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

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

      W is Subspace of V by Th24;

      hence thesis;

    end;

    definition

      let V;

      :: RLSUB_1:def3

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

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

      correctness by Th4, Th30, Th35;

    end

    definition

      let V;

      :: RLSUB_1:def4

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

      coherence

      proof

        set W = the RLSStruct 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;

        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 a be Real holds for 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;



         A6: for a,b be Real holds for 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;



         A7: for a,b be Real holds for 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;



         A8: for a holds for 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);



         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;

        for v be VECTOR of W holds (1 * v) = v

        proof

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;



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

          .= v by RLVECT_1:def 8;

        end;

        then

        reconsider W as RealLinearSpace by A9, A1, A2, A3, A5, A7, A6, 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;



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

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

        hence thesis by A10, Def2;

      end;

    end

    theorem :: RLSUB_1:36



     Th36: ( (0). W) = ( (0). V)

    proof

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

      then

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

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

      hence thesis by A1, Th30;

    end;

    theorem :: RLSUB_1:37



     Th37: ( (0). W1) = ( (0). W2)

    proof

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

      hence thesis by Th36;

    end;

    theorem :: RLSUB_1:38

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

    theorem :: RLSUB_1:39

    ( (0). V) is Subspace of W

    proof

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

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

      hence thesis by Th28;

    end;

    theorem :: RLSUB_1:40

    ( (0). W1) is Subspace of W2

    proof

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

      hence thesis;

    end;

    theorem :: RLSUB_1:41

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

    definition

      let V;

      let v, W;

      :: RLSUB_1:def5

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

      coherence

      proof

        set Y = { (v + u) : u in W };

        defpred P[ object] means ex u 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 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 st x = (v + u) & u in W by A1;

          hence thesis;

        end;

        hence thesis by A2, XBOOLE_0:def 10;

      end;

    end



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

    proof

      set A = { (( 0. V) + u) : 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 Th9;

        then

        reconsider y = x as Element of V;

        (( 0. V) + y) = x;

        hence thesis by A2;

      end;

      A c= the carrier of W

      proof

        let x be object;

        assume x in A;

        then

        consider u such that

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

         A4: u in W;

        x = u by A3;

        hence thesis by A4;

      end;

      hence thesis by A1;

    end;

    definition

      let V;

      let W;

      :: RLSUB_1:def6

      mode Coset of W -> Subset of V means

      : Def6: ex v st it = (v + W);

      existence

      proof

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

        take VW;

        take ( 0. V);

        thus thesis by Lm2;

      end;

    end

    reserve B,C for Coset of W;

    theorem :: RLSUB_1:42



     Th42: ( 0. V) in (v + W) iff v in W

    proof

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

      proof

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

        then

        consider u such that

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

         A2: u in W;

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

        hence thesis by A2, Th22;

      end;

      assume v in W;

      then

       A3: ( - v) in W by Th22;

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

      .= (v + ( - v));

      hence thesis by A3;

    end;

    theorem :: RLSUB_1:43



     Th43: v in (v + W)

    proof

      (v + ( 0. V)) = v & ( 0. V) in W by Th17;

      hence thesis;

    end;

    theorem :: RLSUB_1:44

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

    theorem :: RLSUB_1:45



     Th45: (v + ( (0). V)) = {v}

    proof

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

      proof

        let x be object;

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

        then

        consider u such that

         A1: x = (v + u) and

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



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

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

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

        then x = v by A1;

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

      hence thesis by A4;

    end;



     Lm3: v in W iff (v + W) = the carrier of W

    proof

      ( 0. V) in W & (v + ( 0. V)) = v by Th17;

      then

       A1: v in { (v + u) : 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 such that

           A3: x = (v + u) and

           A4: u in W;

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

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



         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;

        (y - z) in W;

        then

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

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

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

        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 :: RLSUB_1:46



     Th46: (v + ( (Omega). V)) = the carrier of V by STRUCT_0:def 5, Lm3;

    theorem :: RLSUB_1:47



     Th47: ( 0. V) in (v + W) iff (v + W) = the carrier of W by Th42, Lm3;

    theorem :: RLSUB_1:48

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

    theorem :: RLSUB_1:49



     Th49: v in W implies ((a * v) + W) = the carrier of W

    proof

      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 such that

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

         A3: u in W;

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

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

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

      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;

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

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

      hence thesis by A6;

    end;

    theorem :: RLSUB_1:50



     Th50: a <> 0 & ((a * v) + W) = the carrier of W implies v in W

    proof

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

      ( 0. V) in W & ((a * v) + ( 0. V)) = (a * v) by Th17;

      then (a * v) in { ((a * v) + u) : u in W };

      hence contradiction by A2, A3;

    end;

    theorem :: RLSUB_1:51



     Th51: v in W iff (( - v) + W) = the carrier of W

    proof

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

      hence thesis by RLVECT_1: 16;

    end;

    theorem :: RLSUB_1:52



     Th52: u in W iff (v + W) = ((v + u) + W)

    proof

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

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

          hence thesis by A4;

        end;

        let x be object;

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

        then

        consider v2 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, Th20;

        hence thesis by A7;

      end;

      assume

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

      ( 0. V) in W & (v + ( 0. V)) = v by Th17;

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

      then

      consider u1 such that

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

       A10: u1 in W;

      v = (v + ( 0. V)) & v = (v + (u + u1)) by A9, 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, Th22;

    end;

    theorem :: RLSUB_1:53

    u in W iff (v + W) = ((v - u) + W)

    proof



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

      proof

        assume ( - u) in W;

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

        hence thesis;

      end;

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

      hence thesis by A1, Th22;

    end;

    theorem :: RLSUB_1:54



     Th54: v in (u + W) iff (u + W) = (v + W)

    proof

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



          then

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

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

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

          hence thesis by A5;

        end;

        let x be object;

        assume x in (v + W);

        then

        consider v2 such that

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

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

        hence thesis;

      end;

      thus thesis by Th43;

    end;

    theorem :: RLSUB_1:55



     Th55: (v + W) = (( - v) + W) iff v in W

    proof

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

      proof

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

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

        then

        consider u such that

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

         A2: u in W;

        reconsider dwa = 2 as Real;

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

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

        .= ((v + v) - u)

        .= (((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 = ((dwa " ) * u) by RLVECT_1:def 8;

        hence thesis by A2, Th21;

      end;

      assume

       A3: v in W;

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

      hence thesis by A3, Th51;

    end;

    theorem :: RLSUB_1:56



     Th56: u in (v1 + W) & u in (v2 + W) implies (v1 + W) = (v2 + W)

    proof

      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 such that

         A7: x = (v1 + u1) and

         A8: u1 in W;

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

        then

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

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

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

        .= v1;



        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 such that

       A10: x = (v2 + u1) and

       A11: u1 in W;

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

      then

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

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

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

      .= v2;



      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 :: RLSUB_1:57

    u in (v + W) & u in (( - v) + W) implies v in W by Th56, Th55;

    theorem :: RLSUB_1:58



     Th58: a <> 1 & (a * v) in (v + W) implies v in W

    proof

      assume that

       A1: a <> 1 and

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



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

      consider u such that

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

       A5: u in W by A2;

      u = (u + ( 0. V))

      .= (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, Th21;

    end;

    theorem :: RLSUB_1:59



     Th59: v in W implies (a * v) in (v + W)

    proof

      assume v in W;

      then

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

      (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 :: RLSUB_1:60

    ( - v) in (v + W) iff v in W

    proof

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

      hence thesis by Th58, Th59;

    end;

    theorem :: RLSUB_1:61



     Th61: (u + v) in (v + W) iff u in W

    proof

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

      proof

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

        then ex v1 st (u + v) = (v + v1) & v1 in W;

        hence thesis by RLVECT_1: 8;

      end;

      assume u in W;

      hence thesis;

    end;

    theorem :: RLSUB_1:62

    (v - u) in (v + W) iff u in W

    proof



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



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

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

      hence thesis by A1, A2, Th61;

    end;

    theorem :: RLSUB_1:63



     Th63: u in (v + W) iff ex v1 st v1 in W & u = (v + v1)

    proof

      thus u in (v + W) implies ex v1 st v1 in W & u = (v + v1)

      proof

        assume u in (v + W);

        then ex v1 st u = (v + v1) & v1 in W;

        hence thesis;

      end;

      given v1 such that

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

      thus thesis by A1;

    end;

    theorem :: RLSUB_1:64

    u in (v + W) iff ex v1 st v1 in W & u = (v - v1)

    proof

      thus u in (v + W) implies ex v1 st v1 in W & u = (v - v1)

      proof

        assume u in (v + W);

        then

        consider v1 such that

         A1: u = (v + v1) and

         A2: v1 in W;

        take x = ( - v1);

        thus x in W by A2, Th22;

        thus thesis by A1;

      end;

      given v1 such that

       A3: v1 in W and

       A4: u = (v - v1);

      ( - v1) in W by A3, Th22;

      hence thesis by A4;

    end;

    theorem :: RLSUB_1:65



     Th65: (ex v st v1 in (v + W) & v2 in (v + W)) iff (v1 - v2) in W

    proof

      thus (ex v st v1 in (v + W) & v2 in (v + W)) implies (v1 - v2) in W

      proof

        given v such that

         A1: v1 in (v + W) and

         A2: v2 in (v + W);

        consider u2 such that

         A3: u2 in W and

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

        consider u1 such that

         A5: u1 in W and

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

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

        hence thesis by A5, A3, Th23;

      end;

      assume (v1 - v2) in W;

      then

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

      take v1;

      thus v1 in (v1 + W) by Th43;

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

      hence thesis by A7;

    end;

    theorem :: RLSUB_1:66



     Th66: (v + W) = (u + W) implies ex v1 st v1 in W & (v + v1) = u

    proof

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

      then v in (u + W) by Th43;

      then

      consider u1 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, Th22;



      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;

    end;

    theorem :: RLSUB_1:67



     Th67: (v + W) = (u + W) implies ex v1 st v1 in W & (v - v1) = u

    proof

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

      then u in (v + W) by Th43;

      then

      consider u1 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, Th22;



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

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

      .= u;

    end;

    theorem :: RLSUB_1:68



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

    proof

      let W1,W2 be strict Subspace 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 Def2;

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

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

      end;

      thus thesis;

    end;

    theorem :: RLSUB_1:69



     Th69: for W1,W2 be strict Subspace of V holds (v + W1) = (u + W2) implies W1 = W2

    proof

      let W1,W2 be strict Subspace 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 Th9;

        then

        reconsider x as Element of V;

        set z = (v + x);

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

        then

        consider u1 such that

         A5: z = (u + u1) and

         A6: u1 in W2;

        x = (( 0. V) + x)

        .= ((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, Th52;

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

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

        .= (u + u1);

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

        hence thesis by A2, Th68;

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

        then

        reconsider x as Element of V;

        set z = (u + x);

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

        then

        consider u1 such that

         A10: z = (v + u1) and

         A11: u1 in W1;

        x = (( 0. V) + x)

        .= ((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, Th52;

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

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

        .= (v + u1);

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

        hence thesis by A2, Th68;

      end;

      V1 <> V2 by A2, Th30;

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

      hence thesis by A3, A8, XBOOLE_1: 37;

    end;

    theorem :: RLSUB_1:70

    C is linearly-closed iff C = the carrier of W

    proof

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

      proof

        assume

         A1: C is linearly-closed;

        consider v such that

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

        C <> {} by A2, Th43;

        then ( 0. V) in (v + W) by A1, A2, Th1;

        hence thesis by A2, Th47;

      end;

      thus thesis by Lm1;

    end;

    theorem :: RLSUB_1:71

    for 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 W1,W2 be strict Subspace of V, C1 be Coset of W1, C2 be Coset of W2;

      (ex v1 st C1 = (v1 + W1)) & ex v2 st C2 = (v2 + W2) by Def6;

      hence thesis by Th69;

    end;

    theorem :: RLSUB_1:72

     {v} is Coset of ( (0). V)

    proof

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

      hence thesis by Def6;

    end;

    theorem :: RLSUB_1:73

    V1 is Coset of ( (0). V) implies ex v st V1 = {v}

    proof

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

      then

      consider v such that

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

      take v;

      thus thesis by A1, Th45;

    end;

    theorem :: RLSUB_1:74

    the carrier of W is Coset of W

    proof

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

      hence thesis by Def6;

    end;

    theorem :: RLSUB_1:75

    the carrier of V is Coset of ( (Omega). V)

    proof

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

      hence thesis by Def6;

    end;

    theorem :: RLSUB_1:76

    V1 is Coset of ( (Omega). V) implies V1 = the carrier of V

    proof

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

      then ex v st V1 = (v + ( (Omega). V)) by Def6;

      hence thesis by Th46;

    end;

    theorem :: RLSUB_1:77

    ( 0. V) in C iff C = the carrier of W

    proof

      ex v st C = (v + W) by Def6;

      hence thesis by Th47;

    end;

    theorem :: RLSUB_1:78



     Th78: u in C iff C = (u + W)

    proof

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

      proof

        assume

         A1: u in C;

        ex v st C = (v + W) by Def6;

        hence thesis by A1, Th54;

      end;

      thus thesis by Th43;

    end;

    theorem :: RLSUB_1:79

    u in C & v in C implies ex v1 st v1 in W & (u + v1) = v

    proof

      assume u in C & v in C;

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

      hence thesis by Th66;

    end;

    theorem :: RLSUB_1:80

    u in C & v in C implies ex v1 st v1 in W & (u - v1) = v

    proof

      assume u in C & v in C;

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

      hence thesis by Th67;

    end;

    theorem :: RLSUB_1:81

    (ex C st v1 in C & v2 in C) iff (v1 - v2) in W

    proof

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

      proof

        given C such that

         A1: v1 in C & v2 in C;

        ex v st C = (v + W) by Def6;

        hence thesis by A1, Th65;

      end;

      assume (v1 - v2) in W;

      then

      consider v such that

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

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

      take C;

      thus thesis by A2;

    end;

    theorem :: RLSUB_1:82

    u in B & u in C implies B = C

    proof

      assume

       A1: u in B & u in C;

      (ex v1 st B = (v1 + W)) & ex v2 st C = (v2 + W) by Def6;

      hence thesis by A1, Th56;

    end;