:: RUSUB_1 semantic presentation

begin

definition
let V be RealUnitarySpace;
mode Subspace of V ->  RealUnitarySpace means :Def1: :: RUSUB_1:def 1
( 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
 ex b1 being RealUnitarySpace st
( the carrier of b1 c= the carrier of V & 0. b1 = 0. V & the addF of b1 = the addF of V || the carrier of b1 & the Mult of b1 = the Mult of V | [:REAL, the carrier of b1:] & the scalar of b1 = the scalar of V || the carrier of b1 )
proof
take  V ; ::_thesis: ( the carrier of V c= the carrier of V & 0. V = 0. V & 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:] & the scalar of V = the scalar of V || the carrier of 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  ( the carrier of V c= the carrier of V & 0. V = 0. V & 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:] & the scalar of V = the scalar of V || the carrier of V ) by A1, RELAT_1:69; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Subspace RUSUB_1:def_1_:_
 for V, b2 being RealUnitarySpace holds
( b2 is Subspace of V iff ( the carrier of b2 c= the carrier of V & 0. b2 = 0. V & the addF of b2 = the addF of V || the carrier of b2 & the Mult of b2 = the Mult of V | [:REAL, the carrier of b2:] & the scalar of b2 = the scalar of V || the carrier of b2 ) );

theorem :: RUSUB_1:1
for V being RealUnitarySpace
for W1, W2 being Subspace of V
for x being set st x in W1 & W1 is Subspace of W2 holds
x in W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V
for x being set st x in W1 & W1 is Subspace of W2 holds
x in W2
let W1, W2 be Subspace of V; ::_thesis: for x being set st x in W1 & W1 is Subspace of W2 holds
x in W2
let x be set ; ::_thesis: ( x in W1 & W1 is Subspace of W2 implies x in W2 )
assume  ( x in W1 & W1 is Subspace of W2 ) ; ::_thesis: x in W2
then  ( x in the carrier of W1 & the carrier of W1 c= the carrier of W2 ) by Def1, STRUCT_0:def_5;
hence  x in W2 by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th2: :: RUSUB_1:2
for V being RealUnitarySpace
for W being Subspace of V
for x being set st x in W holds
x in V
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for x being set st x in W holds
x in V
let W be Subspace of V; ::_thesis: for x being set st x in W holds
x in V
let x be set ; ::_thesis: ( x in W implies x in V )
assume  x in W ; ::_thesis: x in V
then A1: x in the carrier of W by STRUCT_0:def_5;
 the carrier of W c= the carrier of V by Def1;
hence  x in V by A1, STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th3: :: RUSUB_1:3
for V being RealUnitarySpace
for W being Subspace of V
for w being VECTOR of W holds w is VECTOR of V
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for w being VECTOR of W holds w is VECTOR of V
let W be Subspace of V; ::_thesis: for w being VECTOR of W holds w is VECTOR of V
let w be VECTOR of W; ::_thesis: w is VECTOR of V
 w in V by Th2, RLVECT_1:1;
hence  w is VECTOR of V by STRUCT_0:def_5; ::_thesis: verum
end;

theorem :: RUSUB_1:4
for V being RealUnitarySpace
for W being Subspace of V holds 0. W = 0. V by Def1;

theorem :: RUSUB_1:5
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds 0. W1 = 0. W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds 0. W1 = 0. W2
let W1, W2 be Subspace of V; ::_thesis: 0. W1 = 0. W2
 0. W1 = 0. V by Def1;
hence  0. W1 = 0. W2 by Def1; ::_thesis: verum
end;

theorem Th6: :: RUSUB_1:6
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 + w2 = v + u
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 + w2 = v + u
let W be Subspace of V; ::_thesis: for u, v being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 + w2 = v + u
let u, v be VECTOR of V; ::_thesis: for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 + w2 = v + u
let w1, w2 be VECTOR of W; ::_thesis: ( w1 = v & w2 = u implies w1 + w2 = v + u )
assume A1: ( v = w1 & u = w2 ) ; ::_thesis: w1 + w2 = v + u
 w1 + w2 = ( the addF of V || the carrier of W) . [w1,w2] by Def1;
hence  w1 + w2 = v + u by A1, FUNCT_1:49; ::_thesis: verum
end;

theorem Th7: :: RUSUB_1:7
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for w being VECTOR of W
for a being Real st w = v holds
a * w = a * v
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V
for w being VECTOR of W
for a being Real st w = v holds
a * w = a * v
let W be Subspace of V; ::_thesis: for v being VECTOR of V
for w being VECTOR of W
for a being Real st w = v holds
a * w = a * v
let v be VECTOR of V; ::_thesis: for w being VECTOR of W
for a being Real st w = v holds
a * w = a * v
let w be VECTOR of W; ::_thesis: for a being Real st w = v holds
a * w = a * v
let a be Real; ::_thesis: ( w = v implies a * w = a * v )
assume A1: w = v ; ::_thesis: a * w = a * v
 a * w = ( the Mult of V | [:REAL, the carrier of W:]) . [a,w] by Def1;
hence  a * w = a * v by A1, FUNCT_1:49; ::_thesis: verum
end;

theorem :: RUSUB_1:8
for V being RealUnitarySpace
for W being Subspace of V
for v1, v2 being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v1 & w2 = v2 holds
w1 .|. w2 = v1 .|. v2
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v1, v2 being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v1 & w2 = v2 holds
w1 .|. w2 = v1 .|. v2
let W be Subspace of V; ::_thesis: for v1, v2 being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v1 & w2 = v2 holds
w1 .|. w2 = v1 .|. v2
let v1, v2 be VECTOR of V; ::_thesis: for w1, w2 being VECTOR of W st w1 = v1 & w2 = v2 holds
w1 .|. w2 = v1 .|. v2
let w1, w2 be VECTOR of W; ::_thesis: ( w1 = v1 & w2 = v2 implies w1 .|. w2 = v1 .|. v2 )
reconsider ww1 = w1, ww2 = w2 as VECTOR of V by Th3;
assume  ( w1 = v1 & w2 = v2 ) ; ::_thesis: w1 .|. w2 = v1 .|. v2
then A1: v1 .|. v2 = the scalar of V . [ww1,ww2] by BHSP_1:def_1;
w1 .|. w2 = the scalar of W . [w1,w2] by BHSP_1:def_1
.= ( the scalar of V || the carrier of W) . [w1,w2] by Def1 ;
hence  w1 .|. w2 = v1 .|. v2 by A1, FUNCT_1:49; ::_thesis: verum
end;

theorem Th9: :: RUSUB_1:9
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for w being VECTOR of W st w = v holds
- v = - w
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V
for w being VECTOR of W st w = v holds
- v = - w
let W be Subspace of V; ::_thesis: for v being VECTOR of V
for w being VECTOR of W st w = v holds
- v = - w
let v be VECTOR of V; ::_thesis: for w being VECTOR of W st w = v holds
- v = - w
let w be VECTOR of W; ::_thesis: ( w = v implies - v = - w )
A1: ( - v = (- 1) * v & - w = (- 1) * w ) by RLVECT_1:16;
assume  w = v ; ::_thesis: - v = - w
hence  - v = - w by A1, Th7; ::_thesis: verum
end;

theorem Th10: :: RUSUB_1:10
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 - w2 = v - u
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 - w2 = v - u
let W be Subspace of V; ::_thesis: for u, v being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 - w2 = v - u
let u, v be VECTOR of V; ::_thesis: for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 - w2 = v - u
let w1, w2 be VECTOR of W; ::_thesis: ( w1 = v & w2 = u implies w1 - w2 = v - u )
assume that
A1: w1 = v and
A2: w2 = u ; ::_thesis: w1 - w2 = v - u
 - w2 = - u by A2, Th9;
hence  w1 - w2 = v - u by A1, Th6; ::_thesis: verum
end;

theorem Th11: :: RUSUB_1:11
for V being RealUnitarySpace
for W being Subspace of V holds 0. V in W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V holds 0. V in W
let W be Subspace of V; ::_thesis: 0. V in W
 0. W in W by RLVECT_1:1;
hence  0. V in W by Def1; ::_thesis: verum
end;

theorem :: RUSUB_1:12
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds 0. W1 in W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds 0. W1 in W2
let W1, W2 be Subspace of V; ::_thesis: 0. W1 in W2
 0. W1 = 0. V by Def1;
hence  0. W1 in W2 by Th11; ::_thesis: verum
end;

theorem :: RUSUB_1:13
for V being RealUnitarySpace
for W being Subspace of V holds 0. W in V by Th2, RLVECT_1:1;

Lm1:  for V being RealUnitarySpace
for W being Subspace of V
for V1, V2 being Subset of V st the carrier of W = V1 holds
V1 is linearly-closed
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for V1, V2 being Subset of V st the carrier of W = V1 holds
V1 is linearly-closed
let W be Subspace of V; ::_thesis: for V1, V2 being Subset of V st the carrier of W = V1 holds
V1 is linearly-closed
let V1, V2 be Subset of V; ::_thesis: ( the carrier of W = V1 implies V1 is linearly-closed )
set VW = the carrier of W;
reconsider WW = W as RealUnitarySpace ;
assume A1: the carrier of W = V1 ; ::_thesis: V1 is linearly-closed
A2: for a being Real
for v being VECTOR of V st v in V1 holds
a * v in V1
proof
let a be Real; ::_thesis: for v being VECTOR of V st v in V1 holds
a * v in V1
let v be VECTOR of V; ::_thesis: ( v in V1 implies a * v in V1 )
assume  v in V1 ; ::_thesis: a * v in V1
then reconsider vv = v as VECTOR of WW by A1;
reconsider vw = a * vv as Element of the carrier of W ;
 vw in V1 by A1;
hence  a * v in V1 by Th7; ::_thesis: verum
end;
 for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1
proof
let v, u be VECTOR of V; ::_thesis: ( v in V1 & u in V1 implies v + u in V1 )
assume  ( v in V1 & u in V1 ) ; ::_thesis: v + u in V1
then reconsider vv = v, uu = u as VECTOR of WW by A1;
reconsider vw = vv + uu as Element of the carrier of W ;
 vw in V1 by A1;
hence  v + u in V1 by Th6; ::_thesis: verum
end;
hence  V1 is linearly-closed by A2, RLSUB_1:def_1; ::_thesis: verum
end;

theorem Th14: :: RUSUB_1:14
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V st u in W & v in W holds
u + v in W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v being VECTOR of V st u in W & v in W holds
u + v in W
let W be Subspace of V; ::_thesis: for u, v being VECTOR of V st u in W & v in W holds
u + v in W
reconsider VW = the carrier of W as Subset of V by Def1;
let u, v be VECTOR of V; ::_thesis: ( u in W & v in W implies u + v in W )
assume  ( u in W & v in W ) ; ::_thesis: u + v in W
then A1: ( u in the carrier of W & v in the carrier of W ) by STRUCT_0:def_5;
 VW is linearly-closed by Lm1;
then  u + v in the carrier of W by A1, RLSUB_1:def_1;
hence  u + v in W by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th15: :: RUSUB_1:15
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for a being Real st v in W holds
a * v in W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V
for a being Real st v in W holds
a * v in W
let W be Subspace of V; ::_thesis: for v being VECTOR of V
for a being Real st v in W holds
a * v in W
reconsider VW = the carrier of W as Subset of V by Def1;
let v be VECTOR of V; ::_thesis: for a being Real st v in W holds
a * v in W
let a be Real; ::_thesis: ( v in W implies a * v in W )
assume  v in W ; ::_thesis: a * v in W
then A1: v in the carrier of W by STRUCT_0:def_5;
 VW is linearly-closed by Lm1;
then  a * v in the carrier of W by A1, RLSUB_1:def_1;
hence  a * v in W by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th16: :: RUSUB_1:16
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V st v in W holds
- v in W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V st v in W holds
- v in W
let W be Subspace of V; ::_thesis: for v being VECTOR of V st v in W holds
- v in W
let v be VECTOR of V; ::_thesis: ( v in W implies - v in W )
assume  v in W ; ::_thesis: - v in W
then  (- 1) * v in W by Th15;
hence  - v in W by RLVECT_1:16; ::_thesis: verum
end;

theorem Th17: :: RUSUB_1:17
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V st u in W & v in W holds
u - v in W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v being VECTOR of V st u in W & v in W holds
u - v in W
let W be Subspace of V; ::_thesis: for u, v being VECTOR of V st u in W & v in W holds
u - v in W
let u, v be VECTOR of V; ::_thesis: ( u in W & v in W implies u - v in W )
assume that
A1: u in W and
A2: v in W ; ::_thesis: u - v in W
 - v in W by A2, Th16;
hence  u - v in W by A1, Th14; ::_thesis: verum
end;

theorem Th18: :: RUSUB_1:18
for V being RealUnitarySpace
for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:REAL,D:],D
for S being 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; ::_thesis: for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:REAL,D:],D
for S being 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
let V1 be Subset of V; ::_thesis: for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:REAL,D:],D
for S being 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
let D be non empty set ; ::_thesis: for d1 being Element of D
for A being BinOp of D
for M being Function of [:REAL,D:],D
for S being 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
let d1 be Element of D; ::_thesis: for A being BinOp of D
for M being Function of [:REAL,D:],D
for S being 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
let A be BinOp of D; ::_thesis: for M being Function of [:REAL,D:],D
for S being 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
let M be Function of [:REAL,D:],D; ::_thesis: for S being 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
let S be Function of [:D,D:],REAL; ::_thesis: ( V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] & S = the scalar of V || V1 implies UNITSTR(# D,d1,A,M,S #) is Subspace of V )
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 ; ::_thesis: UNITSTR(# D,d1,A,M,S #) is Subspace of V
 UNITSTR(# D,d1,A,M,S #) is Subspace of V
proof
set W = UNITSTR(# D,d1,A,M,S #);
A6: for a being Real
for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds a * x = the Mult of V . [a,x] by A1, A4, FUNCT_1:49;
A7: for x, y being VECTOR of UNITSTR(# D,d1,A,M,S #) holds x .|. y = the scalar of V . [x,y]
proof
let x, y be VECTOR of UNITSTR(# D,d1,A,M,S #); ::_thesis: x .|. y = the scalar of V . [x,y]
 x .|. y = ( the scalar of V || the carrier of UNITSTR(# D,d1,A,M,S #)) . [x,y] by A1, A5, BHSP_1:def_1;
hence  x .|. y = the scalar of V . [x,y] by FUNCT_1:49; ::_thesis: verum
end;
A8: for x, y being VECTOR of UNITSTR(# D,d1,A,M,S #) holds x + y = the addF of V . [x,y] by A1, A3, FUNCT_1:49;
A9: ( UNITSTR(# D,d1,A,M,S #) is RealUnitarySpace-like & UNITSTR(# D,d1,A,M,S #) is vector-distributive & UNITSTR(# D,d1,A,M,S #) is scalar-distributive & UNITSTR(# D,d1,A,M,S #) is scalar-associative & UNITSTR(# D,d1,A,M,S #) is scalar-unital & UNITSTR(# D,d1,A,M,S #) is Abelian & UNITSTR(# D,d1,A,M,S #) is add-associative & UNITSTR(# D,d1,A,M,S #) is right_zeroed & UNITSTR(# D,d1,A,M,S #) is right_complementable )
proof
set SV = the scalar of V;
set MV = the Mult of V;
set AV = the addF of V;
A10: for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds 1 * x = x
proof
let x be VECTOR of UNITSTR(# D,d1,A,M,S #); ::_thesis: 1 * x = x
reconsider y = x as VECTOR of V by A1, TARSKI:def_3;
thus 1 * x = 1 * y by A6
.= x by RLVECT_1:def_8 ; ::_thesis: verum
end;
A11: for a, b being real number
for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds (a * b) * x = a * (b * x)
proof
let a, b be real number ; ::_thesis: for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds (a * b) * x = a * (b * x)
let x be VECTOR of UNITSTR(# D,d1,A,M,S #); ::_thesis: (a * b) * x = a * (b * x)
reconsider y = x as VECTOR of V by A1, TARSKI:def_3;
reconsider a = a, b = b as Real by XREAL_0:def_1;
(a * b) * x = (a * b) * y by A6
.= a * (b * y) by RLVECT_1:def_7
.= the Mult of V . [a,(b * x)] by A6
.= a * (b * x) by A1, A4, FUNCT_1:49 ;
hence  (a * b) * x = a * (b * x) ; ::_thesis: verum
end;
A12: for a being real number
for x, y being VECTOR of UNITSTR(# D,d1,A,M,S #) holds a * (x + y) = (a * x) + (a * y)
proof
let a be real number ; ::_thesis: for x, y being VECTOR of UNITSTR(# D,d1,A,M,S #) holds a * (x + y) = (a * x) + (a * y)
let x, y be VECTOR of UNITSTR(# D,d1,A,M,S #); ::_thesis: a * (x + y) = (a * x) + (a * y)
reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def_3;
reconsider a = a as Real by XREAL_0:def_1;
a * (x + y) = the Mult of V . [a,(x + y)] by A1, A4, FUNCT_1:49
.= a * (x1 + y1) by A8
.= (a * x1) + (a * y1) by RLVECT_1:def_5
.= the addF of V . [( the Mult of V . [a,x1]),(a * y)] by A6
.= the addF of V . [(a * x),(a * y)] by A6
.= (a * x) + (a * y) by A1, A3, FUNCT_1:49 ;
hence  a * (x + y) = (a * x) + (a * y) ; ::_thesis: verum
end;
A13: for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds x + (0. UNITSTR(# D,d1,A,M,S #)) = x
proof
let x be VECTOR of UNITSTR(# D,d1,A,M,S #); ::_thesis: x + (0. UNITSTR(# D,d1,A,M,S #)) = x
reconsider y = x as VECTOR of V by A1, TARSKI:def_3;
thus x + (0. UNITSTR(# D,d1,A,M,S #)) = y + (0. V) by A2, A8
.= x by RLVECT_1:4 ; ::_thesis: verum
end;
A14: for x, y, z being VECTOR of UNITSTR(# D,d1,A,M,S #)
for a being Real holds
( ( x .|. x = 0 implies x = 0. UNITSTR(# D,d1,A,M,S #) ) & ( x = 0. UNITSTR(# D,d1,A,M,S #) implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
proof
let x, y, z be VECTOR of UNITSTR(# D,d1,A,M,S #); ::_thesis: for a being Real holds
( ( x .|. x = 0 implies x = 0. UNITSTR(# D,d1,A,M,S #) ) & ( x = 0. UNITSTR(# D,d1,A,M,S #) implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
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; ::_thesis: ( ( x .|. x = 0 implies x = 0. UNITSTR(# D,d1,A,M,S #) ) & ( x = 0. UNITSTR(# D,d1,A,M,S #) implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
A15: the scalar of V . [y1,z1] = y1 .|. z1 by BHSP_1:def_1;
A16: ( x = 0. UNITSTR(# D,d1,A,M,S #) implies x .|. x = 0 )
proof
assume  x = 0. UNITSTR(# D,d1,A,M,S #) ; ::_thesis: x .|. x = 0
then  x1 .|. x1 = 0 by A2, BHSP_1:def_2;
then  the scalar of V . [x1,x1] = 0 by BHSP_1:def_1;
hence  x .|. x = 0 by A7; ::_thesis: verum
end;
 ( x .|. x = 0 implies x = 0. UNITSTR(# D,d1,A,M,S #) )
proof
assume  x .|. x = 0 ; ::_thesis: x = 0. UNITSTR(# D,d1,A,M,S #)
then  the scalar of V . [x1,x1] = 0 by A7;
then  x1 .|. x1 = 0 by BHSP_1:def_1;
hence  x = 0. UNITSTR(# D,d1,A,M,S #) by A2, BHSP_1:def_2; ::_thesis: verum
end;
hence  ( x .|. x = 0 iff x = 0. UNITSTR(# D,d1,A,M,S #) ) by A16; ::_thesis: ( 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
 0 <= x1 .|. x1 by BHSP_1:def_2;
then  0 <= the scalar of V . [x1,x1] by BHSP_1:def_1;
hence  0 <= x .|. x by A7; ::_thesis: ( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
 the scalar of V . [x1,y1] = y1 .|. x1 by BHSP_1:def_1;
then  the scalar of V . [x1,y1] = the scalar of V . [y1,x1] by BHSP_1:def_1;
then  x .|. y = the scalar of V . [y1,x1] by A7;
hence  x .|. y = y .|. x by A7; ::_thesis: ( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
A17: (x + y) .|. z = the scalar of V . [(x + y),z] by A7
.= the scalar of V . [(x1 + y1),z] by A8
.= (x1 + y1) .|. z1 by BHSP_1:def_1
.= (x1 .|. z1) + (y1 .|. z1) by BHSP_1:def_2 ;
(x .|. z) + (y .|. z) = ( the scalar of V . [x,z]) + (y .|. z) by A7
.= ( the scalar of V . [x,z]) + ( the scalar of V . [y,z]) by A7
.= (x1 .|. z1) + (y1 .|. z1) by A15, BHSP_1:def_1 ;
hence  (x + y) .|. z = (x .|. z) + (y .|. z) by A17; ::_thesis: (a * x) .|. y = a * (x .|. y)
A18: a * (x .|. y) = a * ( the scalar of V . [x,y]) by A7
.= a * (x1 .|. y1) by BHSP_1:def_1 ;
(a * x) .|. y = the scalar of V . [(a * x),y] by A7
.= the scalar of V . [(a * x1),y] by A6
.= (a * x1) .|. y1 by BHSP_1:def_1
.= a * (x1 .|. y1) by BHSP_1:def_2 ;
hence  (a * x) .|. y = a * (x .|. y) by A18; ::_thesis: verum
end;
A19: for a, b being real number
for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds (a + b) * x = (a * x) + (b * x)
proof
let a, b be real number ; ::_thesis: for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds (a + b) * x = (a * x) + (b * x)
let x be VECTOR of UNITSTR(# D,d1,A,M,S #); ::_thesis: (a + b) * x = (a * x) + (b * x)
reconsider y = x as VECTOR of V by A1, TARSKI:def_3;
reconsider a = a, b = b as Real by XREAL_0:def_1;
(a + b) * x = (a + b) * y by A6
.= (a * y) + (b * y) by RLVECT_1:def_6
.= the addF of V . [( the Mult of V . [a,y]),(b * x)] by A6
.= the addF of V . [(a * x),(b * x)] by A6
.= (a * x) + (b * x) by A1, A3, FUNCT_1:49 ;
hence  (a + b) * x = (a * x) + (b * x) ; ::_thesis: verum
end;
A20: UNITSTR(# D,d1,A,M,S #) is right_complementable
proof
let x be VECTOR of UNITSTR(# D,d1,A,M,S #); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x1 = x as VECTOR of V by A1, TARSKI:def_3;
consider v being VECTOR of V such that
A21: x1 + v = 0. V by ALGSTR_0:def_11;
v = - x1 by A21, RLVECT_1:def_10
.= (- 1) * x1 by RLVECT_1:16
.= (- 1) * x by A6 ;
then reconsider y = v as VECTOR of UNITSTR(# D,d1,A,M,S #) ;
take  y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. UNITSTR(# D,d1,A,M,S #)
thus  x + y = 0. UNITSTR(# D,d1,A,M,S #) by A2, A8, A21; ::_thesis: verum
end;
A22: for x, y being Element of UNITSTR(# D,d1,A,M,S #) holds x + y = y + x
proof
let x, y be Element of UNITSTR(# D,d1,A,M,S #); ::_thesis: x + y = y + x
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 ; ::_thesis: verum
end;
 for x, y, z being VECTOR of UNITSTR(# D,d1,A,M,S #) holds (x + y) + z = x + (y + z)
proof
let x, y, z be VECTOR of UNITSTR(# D,d1,A,M,S #); ::_thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1, TARSKI:def_3;
thus (x + y) + z = the addF of V . [(x + y),z1] by A8
.= (x1 + y1) + z1 by A8
.= x1 + (y1 + z1) by RLVECT_1:def_3
.= the addF of V . [x1,(y + z)] by A8
.= x + (y + z) by A8 ; ::_thesis: verum
end;
hence  ( UNITSTR(# D,d1,A,M,S #) is RealUnitarySpace-like & UNITSTR(# D,d1,A,M,S #) is vector-distributive & UNITSTR(# D,d1,A,M,S #) is scalar-distributive & UNITSTR(# D,d1,A,M,S #) is scalar-associative & UNITSTR(# D,d1,A,M,S #) is scalar-unital & UNITSTR(# D,d1,A,M,S #) is Abelian & UNITSTR(# D,d1,A,M,S #) is add-associative & UNITSTR(# D,d1,A,M,S #) is right_zeroed & UNITSTR(# D,d1,A,M,S #) is right_complementable ) by A22, A13, A20, A12, A19, A11, A10, A14, BHSP_1:def_2, 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; ::_thesis: verum
end;
 0. UNITSTR(# D,d1,A,M,S #) = 0. V by A2;
hence  UNITSTR(# D,d1,A,M,S #) is Subspace of V by A1, A3, A4, A5, A9, Def1; ::_thesis: verum
end;
hence  UNITSTR(# D,d1,A,M,S #) is Subspace of V ; ::_thesis: verum
end;

theorem Th19: :: RUSUB_1:19
for V being RealUnitarySpace holds V is Subspace of V
proof
let V be RealUnitarySpace; ::_thesis: V is Subspace of V
thus  ( the carrier of V c= the carrier of V & 0. V = 0. V ) ; :: according to RUSUB_1:def_1 ::_thesis: ( 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:] & the scalar of V = the scalar of V || the carrier of V )
thus  ( 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:] & the scalar of V = the scalar of V || the carrier of V ) by RELSET_1:19; ::_thesis: verum
end;

theorem Th20: :: RUSUB_1:20
for V, X being strict RealUnitarySpace st V is Subspace of X & X is Subspace of V holds
V = X
proof
let V, X be strict RealUnitarySpace; ::_thesis: ( V is Subspace of X & X is Subspace of V implies V = X )
assume that
A1: V is Subspace of X and
A2: X is Subspace of V ; ::_thesis: V = X
set VX = the carrier of X;
set VV = the carrier of V;
 ( the carrier of V c= the carrier of X & the carrier of X c= the carrier of V ) by A1, A2, Def1;
then A3: the carrier of V = the carrier of X by XBOOLE_0:def_10;
set MX = the Mult of X;
set MV = the Mult of V;
 ( the Mult of V = the Mult of X | [:REAL, the carrier of V:] & the Mult of X = the Mult of V | [:REAL, the carrier of X:] ) by A1, A2, Def1;
then A4: the Mult of V = the Mult of X by A3, RELAT_1:72;
set AX = the addF of X;
set AV = the addF of V;
 ( the addF of V = the addF of X || the carrier of V & the addF of X = the addF of V || the carrier of X ) by A1, A2, Def1;
then A5: the addF of V = the addF of X by A3, RELAT_1:72;
set SX = the scalar of X;
set SV = the scalar of V;
A6: the scalar of X = the scalar of V || the carrier of X by A2, Def1;
 ( 0. V = 0. X & the scalar of V = the scalar of X || the carrier of V ) by A1, Def1;
hence  V = X by A3, A5, A4, A6, RELAT_1:72; ::_thesis: verum
end;

theorem Th21: :: RUSUB_1:21
for V, X, Y being 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; ::_thesis: ( V is Subspace of X & X is Subspace of Y implies V is Subspace of Y )
assume that
A1: V is Subspace of X and
A2: X is Subspace of Y ; ::_thesis: V 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 by XBOOLE_1:1; :: according to RUSUB_1:def_1 ::_thesis: ( 0. V = 0. Y & the addF of V = the addF of Y || the carrier of V & the Mult of V = the Mult of Y | [:REAL, the carrier of V:] & the scalar of V = the scalar of Y || the carrier of V )
 0. V = 0. X by A1, Def1;
hence  0. V = 0. Y by A2, Def1; ::_thesis: ( the addF of V = the addF of Y || the carrier of V & the Mult of V = the Mult of Y | [:REAL, the carrier of V:] & the scalar of V = the scalar of Y || the carrier of V )
thus  the addF of V = the addF of Y || the carrier of V ::_thesis: ( the Mult of V = the Mult of Y | [:REAL, the carrier of V:] & the scalar of V = the scalar 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;
 the carrier of V c= the carrier of X by A1, Def1;
then A3: [: the carrier of V, the carrier of V:] c= [: the carrier of X, the carrier of X:] by ZFMISC_1:96;
 the addF of V = the addF of X || the carrier of V by A1, Def1;
then  the addF of V = ( the addF of Y || the carrier of X) || the carrier of V by A2, Def1;
hence  the addF of V = the addF of Y || the carrier of V by A3, FUNCT_1:51; ::_thesis: verum
end;
thus  the Mult of V = the Mult of Y | [:REAL, the carrier of V:] ::_thesis: the scalar of V = the scalar of Y || 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;
 the carrier of V c= the carrier of X by A1, Def1;
then A4: [:REAL, the carrier of V:] c= [:REAL, the carrier of X:] by ZFMISC_1:95;
 the Mult of V = the Mult of X | [:REAL, the carrier of V:] by A1, Def1;
then  the Mult of V = ( the Mult of Y | [:REAL, the carrier of X:]) | [:REAL, the carrier of V:] by A2, Def1;
hence  the Mult of V = the Mult of Y | [:REAL, the carrier of V:] by A4, FUNCT_1:51; ::_thesis: verum
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;
 the carrier of V c= the carrier of X by A1, Def1;
then A5: [: the carrier of V, the carrier of V:] c= [: the carrier of X, the carrier of X:] by ZFMISC_1:96;
 the scalar of V = the scalar of X || the carrier of V by A1, Def1;
then  the scalar of V = ( the scalar of Y || the carrier of X) || the carrier of V by A2, Def1;
hence  the scalar of V = the scalar of Y || the carrier of V by A5, FUNCT_1:51; ::_thesis: verum
end;

theorem Th22: :: RUSUB_1:22
for V being RealUnitarySpace
for W1, W2 being Subspace of V st the carrier of W1 c= the carrier of W2 holds
W1 is Subspace of W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V st the carrier of W1 c= the carrier of W2 holds
W1 is Subspace of W2
let W1, W2 be Subspace of V; ::_thesis: ( the carrier of W1 c= the carrier of W2 implies W1 is Subspace of W2 )
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 ; ::_thesis: W1 is Subspace of W2
then A2: [: the carrier of W1, the carrier of W1:] c= [: the carrier of W2, the carrier of W2:] 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; :: according to RUSUB_1:def_1 ::_thesis: ( the addF of W1 = the addF of W2 || the carrier of W1 & the Mult of W1 = the Mult of W2 | [:REAL, the carrier of W1:] & the scalar of W1 = the scalar of W2 || the carrier of W1 )
 ( the addF of W1 = the addF of V || the carrier of W1 & the addF of W2 = the addF of V || the carrier of W2 ) by Def1;
hence  the addF of W1 = the addF of W2 || the carrier of W1 by A2, FUNCT_1:51; ::_thesis: ( the Mult of W1 = the Mult of W2 | [:REAL, the carrier of W1:] & the scalar of W1 = the scalar of W2 || the carrier of W1 )
A3: [:REAL, the carrier of W1:] c= [:REAL, the carrier of W2:] by A1, ZFMISC_1:95;
 ( the Mult of W1 = the Mult of V | [:REAL, the carrier of W1:] & the Mult of W2 = the Mult of V | [:REAL, the carrier of W2:] ) by Def1;
hence  the Mult of W1 = the Mult of W2 | [:REAL, the carrier of W1:] by A3, FUNCT_1:51; ::_thesis: the scalar of W1 = the scalar of W2 || the carrier of W1
A4: [: the carrier of W1, the carrier of W1:] c= [: the carrier of W2, the carrier of W2:] by A1, ZFMISC_1:96;
 ( the scalar of W1 = the scalar of V || the carrier of W1 & the scalar of W2 = the scalar of V || the carrier of W2 ) by Def1;
hence  the scalar of W1 = the scalar of W2 || the carrier of W1 by A4, FUNCT_1:51; ::_thesis: verum
end;

theorem :: RUSUB_1:23
for V being RealUnitarySpace
for W1, W2 being Subspace of V st ( for v being VECTOR of V st v in W1 holds
v in W2 ) holds
W1 is Subspace of W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V st ( for v being VECTOR of V st v in W1 holds
v in W2 ) holds
W1 is Subspace of W2
let W1, W2 be Subspace of V; ::_thesis: ( ( for v being VECTOR of V st v in W1 holds
v in W2 ) implies W1 is Subspace of W2 )
assume A1: for v being VECTOR of V st v in W1 holds
v in W2 ; ::_thesis: W1 is Subspace of W2
 the carrier of W1 c= the carrier of W2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of W2 )
assume A2: x in the carrier of W1 ; ::_thesis: x in the carrier of W2
 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, STRUCT_0:def_5;
then  v in W2 by A1;
hence  x in the carrier of W2 by STRUCT_0:def_5; ::_thesis: verum
end;
hence  W1 is Subspace of W2 by Th22; ::_thesis: verum
end;

registration
let V be RealUnitarySpace;
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like for Subspace of V;
existence
 ex b1 being Subspace of V st b1 is strict
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  ex b1 being Subspace of V st b1 is strict ; ::_thesis: verum
end;
end;

theorem Th24: :: RUSUB_1:24
for V being RealUnitarySpace
for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds
W1 = W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds
W1 = W2
let W1, W2 be strict Subspace of V; ::_thesis: ( the carrier of W1 = the carrier of W2 implies W1 = W2 )
assume  the carrier of W1 = the carrier of W2 ; ::_thesis: W1 = W2
then  ( W1 is Subspace of W2 & W2 is Subspace of W1 ) by Th22;
hence  W1 = W2 by Th20; ::_thesis: verum
end;

theorem Th25: :: RUSUB_1:25
for V being RealUnitarySpace
for W1, W2 being strict Subspace of V st ( for v being VECTOR of V holds
( v in W1 iff v in W2 ) ) holds
W1 = W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being strict Subspace of V st ( for v being VECTOR of V holds
( v in W1 iff v in W2 ) ) holds
W1 = W2
let W1, W2 be strict Subspace of V; ::_thesis: ( ( for v being VECTOR of V holds
( v in W1 iff v in W2 ) ) implies W1 = W2 )
assume A1: for v being VECTOR of V holds
( v in W1 iff v in W2 ) ; ::_thesis: W1 = W2
 for x being set holds
( x in the carrier of W1 iff x in the carrier of W2 )
proof
let x be set ; ::_thesis: ( x in the carrier of W1 iff x in the carrier of W2 )
thus  ( x in the carrier of W1 implies x in the carrier of W2 ) ::_thesis: ( x in the carrier of W2 implies x in the carrier of W1 )
proof
assume A2: x in the carrier of W1 ; ::_thesis: x in the carrier of W2
 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, STRUCT_0:def_5;
then  v in W2 by A1;
hence  x in the carrier of W2 by STRUCT_0:def_5; ::_thesis: verum
end;
assume A3: x in the carrier of W2 ; ::_thesis: x in the carrier of W1
 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, STRUCT_0:def_5;
then  v in W1 by A1;
hence  x in the carrier of W1 by STRUCT_0:def_5; ::_thesis: verum
end;
then  the carrier of W1 = the carrier of W2 by TARSKI:1;
hence  W1 = W2 by Th24; ::_thesis: verum
end;

theorem :: RUSUB_1:26
for V being strict RealUnitarySpace
for W being strict Subspace of V st the carrier of W = the carrier of V holds
W = V
proof
let V be strict RealUnitarySpace; ::_thesis: for W being strict Subspace of V st the carrier of W = the carrier of V holds
W = V
let W be strict Subspace of V; ::_thesis: ( the carrier of W = the carrier of V implies W = V )
assume A1: the carrier of W = the carrier of V ; ::_thesis: W = V
 V is Subspace of V by Th19;
hence  W = V by A1, Th24; ::_thesis: verum
end;

theorem :: RUSUB_1:27
for V being strict RealUnitarySpace
for W being strict Subspace of V st ( for v being VECTOR of V holds
( v in W iff v in V ) ) holds
W = V
proof
let V be strict RealUnitarySpace; ::_thesis: for W being strict Subspace of V st ( for v being VECTOR of V holds
( v in W iff v in V ) ) holds
W = V
let W be strict Subspace of V; ::_thesis: ( ( for v being VECTOR of V holds
( v in W iff v in V ) ) implies W = V )
assume A1: for v being VECTOR of V holds
( v in W iff v in V ) ; ::_thesis: W = V
 V is Subspace of V by Th19;
hence  W = V by A1, Th25; ::_thesis: verum
end;

theorem :: RUSUB_1:28
for V being RealUnitarySpace
for W being Subspace of V
for V1 being Subset of V st the carrier of W = V1 holds
V1 is linearly-closed by Lm1;

theorem Th29: :: RUSUB_1:29
for V being RealUnitarySpace
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Subspace of V st V1 = the carrier of W
proof
let V be RealUnitarySpace; ::_thesis: for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Subspace of V st V1 = the carrier of W
let V1 be Subset of V; ::_thesis: ( V1 <> {} & V1 is linearly-closed implies ex W being strict Subspace of V st V1 = the carrier of W )
assume that
A1: V1 <> {} and
A2: V1 is linearly-closed ; ::_thesis: ex W being strict Subspace of V st V1 = the carrier of W
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, the carrier of V:] by FUNCT_2:def_1;
then A3: dom ( the Mult of V | [:REAL,V1:]) = [:REAL, the carrier of V:] /\ [:REAL,V1:] by RELAT_1:61;
 [:REAL,V1:] c= [:REAL, the carrier of V:] by ZFMISC_1:95;
then A4: dom ( the Mult of V | [:REAL,V1:]) = [:REAL,D:] by A3, XBOOLE_1:28;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_D_implies_ex_x_being_set_st_
(_x_in_dom_(_the_Mult_of_V_|_[:REAL,V1:])_&_y_=_(_the_Mult_of_V_|_[:REAL,V1:])_._x_)_)_&_(_ex_x_being_set_st_
(_x_in_dom_(_the_Mult_of_V_|_[:REAL,V1:])_&_y_=_(_the_Mult_of_V_|_[:REAL,V1:])_._x_)_implies_y_in_D_)_)
let y be set ; ::_thesis: ( ( y in D implies ex x being set st
( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) ) & ( ex x being set st
( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) implies y in D ) )
thus  ( y in D implies ex x being set st
( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) ) ::_thesis: ( ex x being set st
( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) implies y in D )
proof
assume A5: y in D ; ::_thesis: ex x being set st
( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x )
then reconsider v1 = y as Element of the carrier of V ;
A6: [1,y] in [:REAL,D:] by A5, ZFMISC_1:87;
then ( the Mult of V | [:REAL,V1:]) . [1,y] = 1 * v1 by FUNCT_1:49
.= y by RLVECT_1:def_8 ;
hence  ex x being set st
( x in dom ( the Mult of V | [:REAL,V1:]) & y = ( the Mult of V | [:REAL,V1:]) . x ) by A4, A6; ::_thesis: verum
end;
given x being set  such that A7: x in dom ( the Mult of V | [:REAL,V1:]) and
A8: y = ( the Mult of V | [:REAL,V1:]) . x ; ::_thesis: y in D
consider x1, x2 being set  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 the carrier of V 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; ::_thesis: verum
end;
then  D = rng ( the Mult of V | [:REAL,V1:]) by FUNCT_1:def_3;
then reconsider M = the Mult of V | [:REAL,V1:] 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 = [: the carrier of V, the carrier of V:] by FUNCT_2:def_1;
then A12: dom ( the addF of V || V1) = [: the carrier of V, the carrier of V:] /\ [:V1,V1:] by RELAT_1:61;
then reconsider S = the scalar of V || V1 as Function of [:D,D:],REAL by FUNCT_2:32;
A13: dom ( the addF of V || V1) = [:D,D:] by A12, XBOOLE_1:28;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_D_implies_ex_x_being_set_st_
(_x_in_dom_(_the_addF_of_V_||_V1)_&_y_=_(_the_addF_of_V_||_V1)_._x_)_)_&_(_ex_x_being_set_st_
(_x_in_dom_(_the_addF_of_V_||_V1)_&_y_=_(_the_addF_of_V_||_V1)_._x_)_implies_y_in_D_)_)
let y be set ; ::_thesis: ( ( y in D implies ex x being set st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) ) & ( ex x being set st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) implies y in D ) )
thus  ( y in D implies ex x being set st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) ) ::_thesis: ( ex x being set st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) implies y in D )
proof
assume A14: y in D ; ::_thesis: ex x being set st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x )
then reconsider v1 = y, v0 = d1 as Element of the carrier of V ;
A15: [d1,y] in [:D,D:] by A14, ZFMISC_1:87;
then ( the addF of V || V1) . [d1,y] = v0 + v1 by FUNCT_1:49
.= y by RLVECT_1:4 ;
hence  ex x being set st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) by A13, A15; ::_thesis: verum
end;
given x being set  such that A16: x in dom ( the addF of V || V1) and
A17: y = ( the addF of V || V1) . x ; ::_thesis: y in D
consider x1, x2 being set  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 the carrier of V 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; ::_thesis: verum
end;
then  D = rng ( the addF of V || V1) by FUNCT_1:def_3;
then reconsider A = the addF of V || V1 as Function of [:D,D:],D by A13, FUNCT_2:def_1, RELSET_1:4;
set W = UNITSTR(# D,d1,A,M,S #);
 UNITSTR(# D,d1,A,M,S #) is Subspace of V by Th18;
hence  ex W being strict Subspace of V st V1 = the carrier of W ; ::_thesis: verum
end;

begin

definition
let V be RealUnitarySpace;
func (0). V ->  strict Subspace of V means :Def2: :: RUSUB_1:def 2
 the carrier of it = {(0. V)};
correctness
existence
ex b1 being strict Subspace of V st the carrier of b1 = {(0. V)};
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = {(0. V)} & the carrier of b2 = {(0. V)} holds
b1 = b2;
by Th24, Th29, RLSUB_1:4;
end;

:: deftheorem Def2 defines (0). RUSUB_1:def_2_:_
 for V being RealUnitarySpace
for b2 being strict Subspace of V holds
( b2 = (0). V iff the carrier of b2 = {(0. V)} );

definition
let V be RealUnitarySpace;
func (Omega). V ->  strict Subspace of V equals :: RUSUB_1:def 3
 UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #);
coherence
 UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict Subspace of V
proof
set W = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #);
A1: for u, v, w being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds (u + v) + w = u + (v + w)
proof
let u, v, w be VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #); ::_thesis: (u + v) + w = u + (v + 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) ; ::_thesis: verum
end;
A2: for v being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds v + (0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #)) = v
proof
let v be VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #); ::_thesis: v + (0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #)) = v
reconsider v9 = v as VECTOR of V ;
thus v + (0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #)) = v9 + (0. V)
.= v by RLVECT_1:4 ; ::_thesis: verum
end;
A3: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is right_complementable
proof
let v be VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider v9 = v as VECTOR of V ;
consider w9 being VECTOR of V such that
A4: v9 + w9 = 0. V by ALGSTR_0:def_11;
reconsider w = w9 as VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #)
thus  v + w = 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by A4; ::_thesis: verum
end;
A5: for v being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds 1 * v = v
proof
let v be VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #); ::_thesis: 1 * v = v
reconsider v9 = v as VECTOR of V ;
thus 1 * v = 1 * v9
.= v by RLVECT_1:def_8 ; ::_thesis: verum
end;
A6: for a, b being real number
for v being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds (a + b) * v = (a * v) + (b * v)
proof
let a, b be real number ; ::_thesis: for v being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #); ::_thesis: (a + b) * v = (a * v) + (b * v)
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) ; ::_thesis: verum
end;
A7: for a being real number
for v, w being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds a * (v + w) = (a * v) + (a * w)
proof
let a be real number ; ::_thesis: for v, w being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #); ::_thesis: a * (v + w) = (a * v) + (a * 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) ; ::_thesis: verum
end;
A8: now__::_thesis:_for_a_being_Real
for_v,_w_being_VECTOR_of_UNITSTR(#_the_carrier_of_V,_the_ZeroF_of_V,_the_addF_of_V,_the_Mult_of_V,_the_scalar_of_V_#)
for_v9,_w9_being_VECTOR_of_V_st_v_=_v9_&_w_=_w9_holds_
(_v_+_w_=_v9_+_w9_&_a_*_v_=_a_*_v9_&_v_.|._w_=_v9_.|._w9_)
let a be Real; ::_thesis: for v, w being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #)
for v9, w9 being VECTOR of V st v = v9 & w = w9 holds
( v + w = v9 + w9 & a * v = a * v9 & v .|. w = v9 .|. w9 )
let v, w be VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #); ::_thesis: for v9, w9 being VECTOR of V st v = v9 & w = w9 holds
( v + w = v9 + w9 & a * v = a * v9 & v .|. w = v9 .|. w9 )
let v9, w9 be VECTOR of V; ::_thesis: ( v = v9 & w = w9 implies ( v + w = v9 + w9 & a * v = a * v9 & v .|. w = v9 .|. w9 ) )
assume that
A9: v = v9 and
A10: w = w9 ; ::_thesis: ( v + w = v9 + w9 & a * v = a * v9 & v .|. w = v9 .|. w9 )
thus  v + w = v9 + w9 by A9, A10; ::_thesis: ( a * v = a * v9 & v .|. w = v9 .|. w9 )
thus  a * v = a * v9 by A9; ::_thesis: v .|. w = v9 .|. w9
thus v .|. w = the scalar of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) . [v,w] by BHSP_1:def_1
.= v9 .|. w9 by A9, A10, BHSP_1:def_1 ; ::_thesis: verum
end;
A11: for v, w being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds v + w = w + v
proof
let v, w be VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #); ::_thesis: v + w = w + v
reconsider v9 = v, w9 = w as VECTOR of V ;
thus v + w = w9 + v9 by A8
.= w + v ; ::_thesis: verum
end;
A12: 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = 0. V ;
A13: for x, y, z being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #)
for a being Real holds
( ( x .|. x = 0 implies x = 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ) & ( x = 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
proof
let x, y, z be VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #); ::_thesis: for a being Real holds
( ( x .|. x = 0 implies x = 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ) & ( x = 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
let a be Real; ::_thesis: ( ( x .|. x = 0 implies x = 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ) & ( x = 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
reconsider x9 = x as VECTOR of V ;
reconsider y9 = y as VECTOR of V ;
reconsider z9 = z as VECTOR of V ;
A14: (x + y) .|. z = (x9 + y9) .|. z9 by A8
.= (x9 .|. z9) + (y9 .|. z9) by BHSP_1:def_2 ;
 x9 .|. x9 = x .|. x by A8;
hence  ( x .|. x = 0 iff x = 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ) by A12, BHSP_1:def_2; ::_thesis: ( 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
 x9 .|. x9 = x .|. x by A8;
hence  0 <= x .|. x by BHSP_1:def_2; ::_thesis: ( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
 x9 .|. y9 = x .|. y by A8;
hence  x .|. y = y .|. x by A8; ::_thesis: ( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
 x9 .|. z9 = x .|. z by A8;
hence  (x + y) .|. z = (x .|. z) + (y .|. z) by A8, A14; ::_thesis: (a * x) .|. y = a * (x .|. y)
(a * x) .|. y = (a * x9) .|. y9 by A8
.= a * (x9 .|. y9) by BHSP_1:def_2 ;
hence  (a * x) .|. y = a * (x .|. y) by A8; ::_thesis: verum
end;
 for a, b being real number
for v being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds (a * b) * v = a * (b * v)
proof
let a, b be real number ; ::_thesis: for v being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds (a * b) * v = a * (b * v)
let v be VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #); ::_thesis: (a * b) * v = a * (b * v)
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) ; ::_thesis: verum
end;
then reconsider W = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) as RealUnitarySpace by A11, A1, A2, A3, A7, A6, A5, A13, BHSP_1:def_2, 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;
A15: ( 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  UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict Subspace of V by A15, Def1; ::_thesis: verum
end;
end;

:: deftheorem  defines (Omega). RUSUB_1:def_3_:_
 for V being RealUnitarySpace holds (Omega). V = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #);

begin

theorem Th30: :: RUSUB_1:30
for V being RealUnitarySpace
for W being Subspace of V holds (0). W = (0). V
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V holds (0). W = (0). V
let W be Subspace of V; ::_thesis: (0). W = (0). 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  (0). W = (0). V by A1, Th24; ::_thesis: verum
end;

theorem Th31: :: RUSUB_1:31
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds (0). W1 = (0). W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds (0). W1 = (0). W2
let W1, W2 be Subspace of V; ::_thesis: (0). W1 = (0). W2
 (0). W1 = (0). V by Th30;
hence  (0). W1 = (0). W2 by Th30; ::_thesis: verum
end;

theorem :: RUSUB_1:32
for V being RealUnitarySpace
for W being Subspace of V holds (0). W is Subspace of V by Th21;

theorem :: RUSUB_1:33
for V being RealUnitarySpace
for W being Subspace of V holds (0). V is Subspace of W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V holds (0). V is Subspace of W
let W be Subspace of V; ::_thesis: (0). V is Subspace of W
the carrier of ((0). V) = {(0. V)} by Def2
.= {(0. W)} by Def1 ;
hence  (0). V is Subspace of W by Th22; ::_thesis: verum
end;

theorem :: RUSUB_1:34
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds (0). W1 is Subspace of W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds (0). W1 is Subspace of W2
let W1, W2 be Subspace of V; ::_thesis: (0). W1 is Subspace of W2
 (0). W1 = (0). W2 by Th31;
hence  (0). W1 is Subspace of W2 ; ::_thesis: verum
end;

theorem :: RUSUB_1:35
for V being strict RealUnitarySpace holds V is Subspace of (Omega). V ;

begin

definition
let V be RealUnitarySpace;
let v be VECTOR of V;
let W be Subspace of V;
funcv + W ->  Subset of V equals :: RUSUB_1:def 4
 {  (v + u) where u is VECTOR of V : u in W  }  ;
coherence
  {  (v + u) where u is VECTOR of V : u in W  }  is Subset of V
proof
set Y =  {  (v + u) where u is VECTOR of V : u in W  }  ;
defpred S1[ set ] means  ex u being VECTOR of V st
( $1 = v + u & u in W );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in the carrier of V & S1[x] ) ) from XBOOLE_0:sch_1();
 X c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the carrier of V )
assume  x in X ; ::_thesis: x in the carrier of V
hence  x in the carrier of V by A1; ::_thesis: verum
end;
then reconsider X = X as Subset of V ;
A2:  {  (v + u) where u is VECTOR of V : u in W  }  c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (v + u) where u is VECTOR of V : u in W  }  or x in X )
assume  x in  {  (v + u) where u is VECTOR of V : u in W  }  ; ::_thesis: x in X
then  ex u being VECTOR of V st
( x = v + u & u in W ) ;
hence  x in X by A1; ::_thesis: verum
end;
 X c=  {  (v + u) where u is VECTOR of V : u in W  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in  {  (v + u) where u is VECTOR of V : u in W  }  )
assume  x in X ; ::_thesis: x in  {  (v + u) where u is VECTOR of V : u in W  }
then  ex u being VECTOR of V st
( x = v + u & u in W ) by A1;
hence  x in  {  (v + u) where u is VECTOR of V : u in W  }  ; ::_thesis: verum
end;
hence   {  (v + u) where u is VECTOR of V : u in W  }  is Subset of V by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem  defines + RUSUB_1:def_4_:_
 for V being RealUnitarySpace
for v being VECTOR of V
for W being Subspace of V holds v + W =  {  (v + u) where u is VECTOR of V : u in W  }  ;

Lm2:  for V being RealUnitarySpace
for W being Subspace of V holds (0. V) + W = the carrier of W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V holds (0. V) + W = the carrier of W
let W be Subspace of V; ::_thesis: (0. V) + W = the carrier of W
set A =  {  ((0. V) + u) where u is VECTOR of V : u in W  }  ;
A1: the carrier of W c=  {  ((0. V) + u) where u is VECTOR of V : u in W  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W or x in  {  ((0. V) + u) where u is VECTOR of V : u in W  }  )
assume  x in the carrier of W ; ::_thesis: x in  {  ((0. V) + u) where u is VECTOR of V : u in W  }
then A2: x in W by STRUCT_0:def_5;
then  x in V by Th2;
then reconsider y = x as Element of V by STRUCT_0:def_5;
 (0. V) + y = x by RLVECT_1:4;
hence  x in  {  ((0. V) + u) where u is VECTOR of V : u in W  }  by A2; ::_thesis: verum
end;
  {  ((0. V) + u) where u is VECTOR of V : u in W  }  c= the carrier of W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  ((0. V) + u) where u is VECTOR of V : u in W  }  or x in the carrier of W )
assume  x in  {  ((0. V) + u) where u is VECTOR of V : u in W  }  ; ::_thesis: x in the carrier of W
then consider u being VECTOR of V such that
A3: x = (0. V) + u and
A4: u in W ;
 x = u by A3, RLVECT_1:4;
hence  x in the carrier of W by A4, STRUCT_0:def_5; ::_thesis: verum
end;
hence  (0. V) + W = the carrier of W by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let V be RealUnitarySpace;
let W be Subspace of V;
mode Coset of W ->  Subset of V means :Def5: :: RUSUB_1:def 5
 ex v being VECTOR of V st it = v + W;
existence
 ex b1 being Subset of V ex v being VECTOR of V st b1 = v + W
proof
reconsider VW = the carrier of W as Subset of V by Def1;
take  VW ; ::_thesis: ex v being VECTOR of V st VW = v + W
take  0. V ; ::_thesis: VW = (0. V) + W
thus  VW = (0. V) + W by Lm2; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Coset RUSUB_1:def_5_:_
 for V being RealUnitarySpace
for W being Subspace of V
for b3 being Subset of V holds
( b3 is Coset of W iff ex v being VECTOR of V st b3 = v + W );

begin

theorem Th36: :: RUSUB_1:36
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( 0. V in v + W iff v in W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V holds
( 0. V in v + W iff v in W )
let W be Subspace of V; ::_thesis: for v being VECTOR of V holds
( 0. V in v + W iff v in W )
let v be VECTOR of V; ::_thesis: ( 0. V in v + W iff v in W )
thus  ( 0. V in v + W implies v in W ) ::_thesis: ( v in W implies 0. V in v + W )
proof
assume  0. V in v + W ; ::_thesis: v in W
then consider u being VECTOR of V such that
A1: 0. V = v + u and
A2: u in W ;
 v = - u by A1, RLVECT_1:def_10;
hence  v in W by A2, Th16; ::_thesis: verum
end;
assume  v in W ; ::_thesis: 0. V in v + W
then A3: - v in W by Th16;
0. V = v - v by RLVECT_1:15
.= v + (- v) ;
hence  0. V in v + W by A3; ::_thesis: verum
end;

theorem Th37: :: RUSUB_1:37
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds v in v + W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V holds v in v + W
let W be Subspace of V; ::_thesis: for v being VECTOR of V holds v in v + W
let v be VECTOR of V; ::_thesis: v in v + W
 ( v + (0. V) = v & 0. V in W ) by Th11, RLVECT_1:4;
hence  v in v + W ; ::_thesis: verum
end;

theorem :: RUSUB_1:38
for V being RealUnitarySpace
for W being Subspace of V holds (0. V) + W = the carrier of W by Lm2;

theorem Th39: :: RUSUB_1:39
for V being RealUnitarySpace
for v being VECTOR of V holds v + ((0). V) = {v}
proof
let V be RealUnitarySpace; ::_thesis: for v being VECTOR of V holds v + ((0). V) = {v}
let v be VECTOR of V; ::_thesis: v + ((0). V) = {v}
thus  v + ((0). V) c= {v} :: according to XBOOLE_0:def_10 ::_thesis: {v} c= v + ((0). V)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + ((0). V) or x in {v} )
assume  x in v + ((0). V) ; ::_thesis: x in {v}
then consider u being 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, STRUCT_0:def_5;
then  u = 0. V by A3, TARSKI:def_1;
then  x = v by A1, RLVECT_1:4;
hence  x in {v} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in v + ((0). V) )
assume  x in {v} ; ::_thesis: x in v + ((0). V)
then A4: x = v by TARSKI:def_1;
 ( 0. V in (0). V & v = v + (0. V) ) by Th11, RLVECT_1:4;
hence  x in v + ((0). V) by A4; ::_thesis: verum
end;

Lm3:  for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( v in W iff v + W = the carrier of W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V holds
( v in W iff v + W = the carrier of W )
let W be Subspace of V; ::_thesis: for v being VECTOR of V holds
( v in W iff v + W = the carrier of W )
let v be VECTOR of V; ::_thesis: ( v in W iff v + W = the carrier of W )
 ( 0. V in W & v + (0. V) = v ) by Th11, RLVECT_1:4;
then A1: v in  {  (v + u) where u is VECTOR of V : u in W  }  ;
thus  ( v in W implies v + W = the carrier of W ) ::_thesis: ( v + W = the carrier of W implies v in W )
proof
assume A2: v in W ; ::_thesis: v + W = the carrier of W
thus  v + W c= the carrier of W :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W c= v + W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W or x in the carrier of W )
assume  x in v + W ; ::_thesis: x in the carrier of W
then consider u being VECTOR of V such that
A3: x = v + u and
A4: u in W ;
 v + u in W by A2, A4, Th14;
hence  x in the carrier of W by A3, STRUCT_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W or x in v + W )
assume  x in the carrier of W ; ::_thesis: x in v + W
then reconsider y = x, z = v as Element of W by A2, STRUCT_0:def_5;
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 by STRUCT_0:def_5;
then A6: y1 - z1 in W by Th10;
 y - z = y1 - z1 by Th10;
then  z1 + (y1 - z1) = x by A5, Th6;
hence  x in v + W by A6; ::_thesis: verum
end;
assume A7: v + W = the carrier of W ; ::_thesis: v in W
assume  not v in W ; ::_thesis: contradiction
hence  contradiction by A7, A1, STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th40: :: RUSUB_1:40
for V being RealUnitarySpace
for v being VECTOR of V holds v + ((Omega). V) = the carrier of V
proof
let V be RealUnitarySpace; ::_thesis: for v being VECTOR of V holds v + ((Omega). V) = the carrier of V
let v be VECTOR of V; ::_thesis: v + ((Omega). V) = the carrier of V
 v in (Omega). V by STRUCT_0:def_5;
hence  v + ((Omega). V) = the carrier of V by Lm3; ::_thesis: verum
end;

theorem Th41: :: RUSUB_1:41
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( 0. V in v + W iff v + W = the carrier of W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V holds
( 0. V in v + W iff v + W = the carrier of W )
let W be Subspace of V; ::_thesis: for v being VECTOR of V holds
( 0. V in v + W iff v + W = the carrier of W )
let v be VECTOR of V; ::_thesis: ( 0. V in v + W iff v + W = the carrier of W )
 ( 0. V in v + W iff v in W ) by Th36;
hence  ( 0. V in v + W iff v + W = the carrier of W ) by Lm3; ::_thesis: verum
end;

theorem :: RUSUB_1:42
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( v in W iff v + W = the carrier of W ) by Lm3;

theorem Th43: :: RUSUB_1:43
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for a being Real st v in W holds
(a * v) + W = the carrier of W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V
for a being Real st v in W holds
(a * v) + W = the carrier of W
let W be Subspace of V; ::_thesis: for v being VECTOR of V
for a being Real st v in W holds
(a * v) + W = the carrier of W
let v be VECTOR of V; ::_thesis: for a being Real st v in W holds
(a * v) + W = the carrier of W
let a be Real; ::_thesis: ( v in W implies (a * v) + W = the carrier of W )
assume A1: v in W ; ::_thesis: (a * v) + W = the carrier of W
thus  (a * v) + W c= the carrier of W :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W c= (a * v) + W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (a * v) + W or x in the carrier of W )
assume  x in (a * v) + W ; ::_thesis: x in the carrier of W
then consider u being 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  x in the carrier of W by A2, STRUCT_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W or x in (a * v) + W )
assume A4: x in the carrier of W ; ::_thesis: x in (a * v) + W
then A5: x in W by STRUCT_0:def_5;
 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  x in (a * v) + W by A6; ::_thesis: verum
end;

theorem Th44: :: RUSUB_1:44
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for a being Real st a <> 0 & (a * v) + W = the carrier of W holds
v in W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V
for a being Real st a <> 0 & (a * v) + W = the carrier of W holds
v in W
let W be Subspace of V; ::_thesis: for v being VECTOR of V
for a being Real st a <> 0 & (a * v) + W = the carrier of W holds
v in W
let v be VECTOR of V; ::_thesis: for a being Real st a <> 0 & (a * v) + W = the carrier of W holds
v in W
let a be Real; ::_thesis: ( a <> 0 & (a * v) + W = the carrier of W implies v in W )
assume that
A1: a <> 0 and
A2: (a * v) + W = the carrier of W ; ::_thesis: v in W
assume  not v in W ; ::_thesis: contradiction
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 is VECTOR of V : u in W  }  ;
hence  contradiction by A2, A3, STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th45: :: RUSUB_1:45
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( v in W iff (- v) + W = the carrier of W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V holds
( v in W iff (- v) + W = the carrier of W )
let W be Subspace of V; ::_thesis: for v being VECTOR of V holds
( v in W iff (- v) + W = the carrier of W )
let v be VECTOR of V; ::_thesis: ( v in W iff (- v) + W = the carrier of W )
 ( v in W iff ((- 1) * v) + W = the carrier of W ) by Th43, Th44;
hence  ( v in W iff (- v) + W = the carrier of W ) by RLVECT_1:16; ::_thesis: verum
end;

theorem Th46: :: RUSUB_1:46
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( u in W iff v + W = (v + u) + W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v being VECTOR of V holds
( u in W iff v + W = (v + u) + W )
let W be Subspace of V; ::_thesis: for u, v being VECTOR of V holds
( u in W iff v + W = (v + u) + W )
let u, v be VECTOR of V; ::_thesis: ( u in W iff v + W = (v + u) + W )
thus  ( u in W implies v + W = (v + u) + W ) ::_thesis: ( v + W = (v + u) + W implies u in W )
proof
assume A1: u in W ; ::_thesis: v + W = (v + u) + W
thus  v + W c= (v + u) + W :: according to XBOOLE_0:def_10 ::_thesis: (v + u) + W c= v + W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W or x in (v + u) + W )
assume  x in v + W ; ::_thesis: x in (v + u) + W
then consider v1 being 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  x in (v + u) + W by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (v + u) + W or x in v + W )
assume  x in (v + u) + W ; ::_thesis: x in v + W
then consider v2 being 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  x in v + W by A7; ::_thesis: verum
end;
assume A8: v + W = (v + u) + W ; ::_thesis: u in 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 being 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  u in W by A10, Th16; ::_thesis: verum
end;

theorem :: RUSUB_1:47
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( u in W iff v + W = (v - u) + W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v being VECTOR of V holds
( u in W iff v + W = (v - u) + W )
let W be Subspace of V; ::_thesis: for u, v being VECTOR of V holds
( u in W iff v + W = (v - u) + W )
let u, v be VECTOR of V; ::_thesis: ( u in W iff v + W = (v - u) + W )
A1: ( - u in W implies u in W )
proof
assume  - u in W ; ::_thesis: u in W
then  - (- u) in W by Th16;
hence  u in W by RLVECT_1:17; ::_thesis: verum
end;
 ( - u in W iff v + W = (v + (- u)) + W ) by Th46;
hence  ( u in W iff v + W = (v - u) + W ) by A1, Th16; ::_thesis: verum
end;

theorem Th48: :: RUSUB_1:48
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( v in u + W iff u + W = v + W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v being VECTOR of V holds
( v in u + W iff u + W = v + W )
let W be Subspace of V; ::_thesis: for u, v being VECTOR of V holds
( v in u + W iff u + W = v + W )
let u, v be VECTOR of V; ::_thesis: ( v in u + W iff u + W = v + W )
thus  ( v in u + W implies u + W = v + W ) ::_thesis: ( u + W = v + W implies v in u + W )
proof
assume  v in u + W ; ::_thesis: u + W = v + W
then consider z being VECTOR of V such that
A1: v = u + z and
A2: z in W ;
thus  u + W c= v + W :: according to XBOOLE_0:def_10 ::_thesis: v + W c= u + W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in u + W or x in v + W )
assume  x in u + W ; ::_thesis: x in v + W
then consider v1 being 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  x in v + W by A5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W or x in u + W )
assume  x in v + W ; ::_thesis: x in u + W
then consider v2 being 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  x in u + W ; ::_thesis: verum
end;
thus  ( u + W = v + W implies v in u + W ) by Th37; ::_thesis: verum
end;

theorem Th49: :: RUSUB_1:49
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( v + W = (- v) + W iff v in W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V holds
( v + W = (- v) + W iff v in W )
let W be Subspace of V; ::_thesis: for v being VECTOR of V holds
( v + W = (- v) + W iff v in W )
let v be VECTOR of V; ::_thesis: ( v + W = (- v) + W iff v in W )
thus  ( v + W = (- v) + W implies v in W ) ::_thesis: ( v in W implies v + W = (- v) + W )
proof
assume  v + W = (- v) + W ; ::_thesis: v in W
then  v in (- v) + W by Th37;
then consider u being 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  v in W by A2, Th15; ::_thesis: verum
end;
assume A3: v in W ; ::_thesis: v + W = (- v) + W
then  v + W = the carrier of W by Lm3;
hence  v + W = (- v) + W by A3, Th45; ::_thesis: verum
end;

theorem Th50: :: RUSUB_1:50
for V being RealUnitarySpace
for W being Subspace of V
for u, v1, v2 being VECTOR of V st u in v1 + W & u in v2 + W holds
v1 + W = v2 + W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v1, v2 being VECTOR of V st u in v1 + W & u in v2 + W holds
v1 + W = v2 + W
let W be Subspace of V; ::_thesis: for u, v1, v2 being VECTOR of V st u in v1 + W & u in v2 + W holds
v1 + W = v2 + W
let u, v1, v2 be VECTOR of V; ::_thesis: ( u in v1 + W & u in v2 + W implies v1 + W = v2 + W )
assume that
A1: u in v1 + W and
A2: u in v2 + W ; ::_thesis: v1 + W = v2 + W
consider x1 being VECTOR of V such that
A3: u = v1 + x1 and
A4: x1 in W by A1;
consider x2 being VECTOR of V such that
A5: u = v2 + x2 and
A6: x2 in W by A2;
thus  v1 + W c= v2 + W :: according to XBOOLE_0:def_10 ::_thesis: v2 + W c= v1 + W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v1 + W or x in v2 + W )
assume  x in v1 + W ; ::_thesis: x in v2 + W
then consider u1 being 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  x in v2 + W by A9; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v2 + W or x in v1 + W )
assume  x in v2 + W ; ::_thesis: x in v1 + W
then consider u1 being 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  x in v1 + W by A12; ::_thesis: verum
end;

theorem :: RUSUB_1:51
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V st u in v + W & u in (- v) + W holds
v in W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v being VECTOR of V st u in v + W & u in (- v) + W holds
v in W
let W be Subspace of V; ::_thesis: for u, v being VECTOR of V st u in v + W & u in (- v) + W holds
v in W
let u, v be VECTOR of V; ::_thesis: ( u in v + W & u in (- v) + W implies v in W )
assume  ( u in v + W & u in (- v) + W ) ; ::_thesis: v in W
then  v + W = (- v) + W by Th50;
hence  v in W by Th49; ::_thesis: verum
end;

theorem Th52: :: RUSUB_1:52
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for a being Real st a <> 1 & a * v in v + W holds
v in W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V
for a being Real st a <> 1 & a * v in v + W holds
v in W
let W be Subspace of V; ::_thesis: for v being VECTOR of V
for a being Real st a <> 1 & a * v in v + W holds
v in W
let v be VECTOR of V; ::_thesis: for a being Real st a <> 1 & a * v in v + W holds
v in W
let a be Real; ::_thesis: ( a <> 1 & a * v in v + W implies v in W )
assume that
A1: a <> 1 and
A2: a * v in v + W ; ::_thesis: v in W
A3: a - 1 <> 0 by A1;
consider u being 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  v in W by A5, Th15; ::_thesis: verum
end;

theorem Th53: :: RUSUB_1:53
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for a being Real st v in W holds
a * v in v + W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V
for a being Real st v in W holds
a * v in v + W
let W be Subspace of V; ::_thesis: for v being VECTOR of V
for a being Real st v in W holds
a * v in v + W
let v be VECTOR of V; ::_thesis: for a being Real st v in W holds
a * v in v + W
let a be Real; ::_thesis: ( v in W implies a * v in v + W )
assume  v in W ; ::_thesis: a * v in v + 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  a * v in v + W by A1; ::_thesis: verum
end;

theorem :: RUSUB_1:54
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( - v in v + W iff v in W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V holds
( - v in v + W iff v in W )
let W be Subspace of V; ::_thesis: for v being VECTOR of V holds
( - v in v + W iff v in W )
let v be VECTOR of V; ::_thesis: ( - v in v + W iff v in W )
 (- 1) * v = - v by RLVECT_1:16;
hence  ( - v in v + W iff v in W ) by Th52, Th53; ::_thesis: verum
end;

theorem Th55: :: RUSUB_1:55
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( u + v in v + W iff u in W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v being VECTOR of V holds
( u + v in v + W iff u in W )
let W be Subspace of V; ::_thesis: for u, v being VECTOR of V holds
( u + v in v + W iff u in W )
let u, v be VECTOR of V; ::_thesis: ( u + v in v + W iff u in W )
thus  ( u + v in v + W implies u in W ) ::_thesis: ( u in W implies u + v in v + W )
proof
assume  u + v in v + W ; ::_thesis: u in W
then  ex v1 being VECTOR of V st
( u + v = v + v1 & v1 in W ) ;
hence  u in W by RLVECT_1:8; ::_thesis: verum
end;
assume  u in W ; ::_thesis: u + v in v + W
hence  u + v in v + W ; ::_thesis: verum
end;

theorem :: RUSUB_1:56
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( v - u in v + W iff u in W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v being VECTOR of V holds
( v - u in v + W iff u in W )
let W be Subspace of V; ::_thesis: for u, v being VECTOR of V holds
( v - u in v + W iff u in W )
let u, v be VECTOR of V; ::_thesis: ( v - u in v + W iff u in W )
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  ( v - u in v + W iff u in W ) by A1, A2, Th55, RLVECT_1:17; ::_thesis: verum
end;

theorem Th57: :: RUSUB_1:57
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v being VECTOR of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) )
let W be Subspace of V; ::_thesis: for u, v being VECTOR of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) )
let u, v be VECTOR of V; ::_thesis: ( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) )
thus  ( u in v + W implies ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) ) ::_thesis: ( ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) implies u in v + W )
proof
assume  u in v + W ; ::_thesis: ex v1 being VECTOR of V st
( v1 in W & u = v + v1 )
then  ex v1 being VECTOR of V st
( u = v + v1 & v1 in W ) ;
hence  ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) ; ::_thesis: verum
end;
given v1 being VECTOR of V such that A1: ( v1 in W & u = v + v1 ) ; ::_thesis: u in v + W
thus  u in v + W by A1; ::_thesis: verum
end;

theorem :: RUSUB_1:58
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v being VECTOR of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) )
let W be Subspace of V; ::_thesis: for u, v being VECTOR of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) )
let u, v be VECTOR of V; ::_thesis: ( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) )
thus  ( u in v + W implies ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) ) ::_thesis: ( ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) implies u in v + W )
proof
assume  u in v + W ; ::_thesis: ex v1 being VECTOR of V st
( v1 in W & u = v - v1 )
then consider v1 being VECTOR of V such that
A1: u = v + v1 and
A2: v1 in W ;
take x = - v1; ::_thesis: ( x in W & u = v - x )
thus  x in W by A2, Th16; ::_thesis: u = v - x
thus  u = v - x by A1, RLVECT_1:17; ::_thesis: verum
end;
given v1 being VECTOR of V such that A3: v1 in W and
A4: u = v - v1 ; ::_thesis: u in v + W
 - v1 in W by A3, Th16;
hence  u in v + W by A4; ::_thesis: verum
end;

theorem Th59: :: RUSUB_1:59
for V being RealUnitarySpace
for W being Subspace of V
for v1, v2 being VECTOR of V holds
( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v1, v2 being VECTOR of V holds
( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
let W be Subspace of V; ::_thesis: for v1, v2 being VECTOR of V holds
( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
let v1, v2 be VECTOR of V; ::_thesis: ( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
thus  ( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) implies v1 - v2 in W ) ::_thesis: ( v1 - v2 in W implies ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) )
proof
given v being VECTOR of V such that A1: v1 in v + W and
A2: v2 in v + W ; ::_thesis: v1 - v2 in W
consider u2 being VECTOR of V such that
A3: u2 in W and
A4: v2 = v + u2 by A2, Th57;
consider u1 being 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  v1 - v2 in W by A5, A3, Th17; ::_thesis: verum
end;
assume  v1 - v2 in W ; ::_thesis: ex v being VECTOR of V st
( v1 in v + W & v2 in v + W )
then A7: - (v1 - v2) in W by Th16;
take  v1 ; ::_thesis: ( v1 in v1 + W & v2 in v1 + W )
thus  v1 in v1 + W by Th37; ::_thesis: v2 in v1 + W
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  v2 in v1 + W by A7; ::_thesis: verum
end;

theorem Th60: :: RUSUB_1:60
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v + v1 = u )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v being VECTOR of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v + v1 = u )
let W be Subspace of V; ::_thesis: for u, v being VECTOR of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v + v1 = u )
let u, v be VECTOR of V; ::_thesis: ( v + W = u + W implies ex v1 being VECTOR of V st
( v1 in W & v + v1 = u ) )
assume  v + W = u + W ; ::_thesis: ex v1 being VECTOR of V st
( v1 in W & v + v1 = u )
then  v in u + W by Th37;
then consider u1 being VECTOR of V such that
A1: v = u + u1 and
A2: u1 in W ;
take v1 = u - v; ::_thesis: ( v1 in W & v + v1 = u )
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; ::_thesis: v + v1 = u
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 ; ::_thesis: verum
end;

theorem Th61: :: RUSUB_1:61
for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v - v1 = u )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u, v being VECTOR of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v - v1 = u )
let W be Subspace of V; ::_thesis: for u, v being VECTOR of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v - v1 = u )
let u, v be VECTOR of V; ::_thesis: ( v + W = u + W implies ex v1 being VECTOR of V st
( v1 in W & v - v1 = u ) )
assume  v + W = u + W ; ::_thesis: ex v1 being VECTOR of V st
( v1 in W & v - v1 = u )
then  u in v + W by Th37;
then consider u1 being VECTOR of V such that
A1: u = v + u1 and
A2: u1 in W ;
take v1 = v - u; ::_thesis: ( v1 in W & v - v1 = 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; ::_thesis: v - v1 = u
thus v - v1 = (v - v) + u by RLVECT_1:29
.= (0. V) + u by RLVECT_1:15
.= u by RLVECT_1:4 ; ::_thesis: verum
end;

theorem Th62: :: RUSUB_1:62
for V being RealUnitarySpace
for W1, W2 being strict Subspace of V
for v being VECTOR of V holds
( v + W1 = v + W2 iff W1 = W2 )
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being strict Subspace of V
for v being VECTOR of V holds
( v + W1 = v + W2 iff W1 = W2 )
let W1, W2 be strict Subspace of V; ::_thesis: for v being VECTOR of V holds
( v + W1 = v + W2 iff W1 = W2 )
let v be VECTOR of V; ::_thesis: ( v + W1 = v + W2 iff W1 = W2 )
thus  ( v + W1 = v + W2 implies W1 = W2 ) ::_thesis: ( W1 = W2 implies v + W1 = v + W2 )
proof
assume A1: v + W1 = v + W2 ; ::_thesis: W1 = 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 :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W2 c= the carrier of W1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of W2 )
assume A3: x in the carrier of W1 ; ::_thesis: x in the carrier of W2
then reconsider y = x as Element of V by A2;
set z = v + y;
 x in W1 by A3, STRUCT_0:def_5;
then  v + y in v + W2 by A1;
then consider u being VECTOR of V such that
A4: v + y = v + u and
A5: u in W2 ;
 y = u by A4, RLVECT_1:8;
hence  x in the carrier of W2 by A5, STRUCT_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W2 or x in the carrier of W1 )
assume A6: x in the carrier of W2 ; ::_thesis: x in the carrier of W1
 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, STRUCT_0:def_5;
then  v + y in v + W1 by A1;
then consider u being VECTOR of V such that
A7: v + y = v + u and
A8: u in W1 ;
 y = u by A7, RLVECT_1:8;
hence  x in the carrier of W1 by A8, STRUCT_0:def_5; ::_thesis: verum
end;
hence  W1 = W2 by Th24; ::_thesis: verum
end;
thus  ( W1 = W2 implies v + W1 = v + W2 ) ; ::_thesis: verum
end;

theorem Th63: :: RUSUB_1:63
for V being RealUnitarySpace
for W1, W2 being strict Subspace of V
for u, v being VECTOR of V st v + W1 = u + W2 holds
W1 = W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being strict Subspace of V
for u, v being VECTOR of V st v + W1 = u + W2 holds
W1 = W2
let W1, W2 be strict Subspace of V; ::_thesis: for u, v being VECTOR of V st v + W1 = u + W2 holds
W1 = W2
let u, v be VECTOR of V; ::_thesis: ( v + W1 = u + W2 implies W1 = W2 )
assume A1: v + W1 = u + W2 ; ::_thesis: W1 = W2
set V2 = the carrier of W2;
set V1 = the carrier of W1;
assume A2: W1 <> W2 ; ::_thesis: contradiction
A3: now__::_thesis:_not_the_carrier_of_W1_\_the_carrier_of_W2_<>_{}
set x = the Element of the carrier of W1 \ the carrier of W2;
assume  the carrier of W1 \ the carrier of W2 <> {} ; ::_thesis: contradiction
then  the Element of the carrier of W1 \ the carrier of W2 in the carrier of W1 by XBOOLE_0:def_5;
then A4: the Element of the carrier of W1 \ the carrier of W2 in W1 by STRUCT_0:def_5;
then  the Element of the carrier of W1 \ the carrier of W2 in V by Th2;
then reconsider x = the Element of the carrier of W1 \ the carrier of W2 as Element of V by STRUCT_0:def_5;
set z = v + x;
 v + x in u + W2 by A1, A4;
then consider u1 being VECTOR of V such that
A5: v + x = 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  contradiction by A2, Th62; ::_thesis: verum
end;
A8: now__::_thesis:_not_the_carrier_of_W2_\_the_carrier_of_W1_<>_{}
set x = the Element of the carrier of W2 \ the carrier of W1;
assume  the carrier of W2 \ the carrier of W1 <> {} ; ::_thesis: contradiction
then  the Element of the carrier of W2 \ the carrier of W1 in the carrier of W2 by XBOOLE_0:def_5;
then A9: the Element of the carrier of W2 \ the carrier of W1 in W2 by STRUCT_0:def_5;
then  the Element of the carrier of W2 \ the carrier of W1 in V by Th2;
then reconsider x = the Element of the carrier of W2 \ the carrier of W1 as Element of V by STRUCT_0:def_5;
set z = u + x;
 u + x in v + W1 by A1, A9;
then consider u1 being VECTOR of V such that
A10: u + x = 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  contradiction by A2, Th62; ::_thesis: verum
end;
 the carrier of W1 <> the carrier of W2 by A2, Th24;
then  ( not the carrier of W1 c= the carrier of W2 or not the carrier of W2 c= the carrier of W1 ) by XBOOLE_0:def_10;
hence  contradiction by A3, A8, XBOOLE_1:37; ::_thesis: verum
end;

theorem :: RUSUB_1:64
for V being RealUnitarySpace
for W being Subspace of V
for C being Coset of W holds
( C is linearly-closed iff C = the carrier of W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for C being Coset of W holds
( C is linearly-closed iff C = the carrier of W )
let W be Subspace of V; ::_thesis: for C being Coset of W holds
( C is linearly-closed iff C = the carrier of W )
let C be Coset of W; ::_thesis: ( C is linearly-closed iff C = the carrier of W )
thus  ( C is linearly-closed implies C = the carrier of W ) ::_thesis: ( C = the carrier of W implies C is linearly-closed )
proof
assume A1: C is linearly-closed ; ::_thesis: C = the carrier of W
consider v being 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  C = the carrier of W by A2, Th41; ::_thesis: verum
end;
thus  ( C = the carrier of W implies C is linearly-closed ) by Lm1; ::_thesis: verum
end;

theorem :: RUSUB_1:65
for V being RealUnitarySpace
for W1, W2 being strict Subspace of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 = C2 holds
W1 = W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being strict Subspace of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 = C2 holds
W1 = W2
let W1, W2 be strict Subspace of V; ::_thesis: for C1 being Coset of W1
for C2 being Coset of W2 st C1 = C2 holds
W1 = W2
let C1 be Coset of W1; ::_thesis: for C2 being Coset of W2 st C1 = C2 holds
W1 = W2
let C2 be Coset of W2; ::_thesis: ( C1 = C2 implies W1 = W2 )
 ( ex v1 being VECTOR of V st C1 = v1 + W1 & ex v2 being VECTOR of V st C2 = v2 + W2 ) by Def5;
hence  ( C1 = C2 implies W1 = W2 ) by Th63; ::_thesis: verum
end;

theorem :: RUSUB_1:66
for V being RealUnitarySpace
for v being VECTOR of V holds {v} is Coset of (0). V
proof
let V be RealUnitarySpace; ::_thesis: for v being VECTOR of V holds {v} is Coset of (0). V
let v be VECTOR of V; ::_thesis: {v} is Coset of (0). V
 v + ((0). V) = {v} by Th39;
hence  {v} is Coset of (0). V by Def5; ::_thesis: verum
end;

theorem :: RUSUB_1:67
for V being RealUnitarySpace
for V1 being Subset of V st V1 is Coset of (0). V holds
ex v being VECTOR of V st V1 = {v}
proof
let V be RealUnitarySpace; ::_thesis: for V1 being Subset of V st V1 is Coset of (0). V holds
ex v being VECTOR of V st V1 = {v}
let V1 be Subset of V; ::_thesis: ( V1 is Coset of (0). V implies ex v being VECTOR of V st V1 = {v} )
assume  V1 is Coset of (0). V ; ::_thesis: ex v being VECTOR of V st V1 = {v}
then consider v being VECTOR of V such that
A1: V1 = v + ((0). V) by Def5;
take  v ; ::_thesis: V1 = {v}
thus  V1 = {v} by A1, Th39; ::_thesis: verum
end;

theorem :: RUSUB_1:68
for V being RealUnitarySpace
for W being Subspace of V holds the carrier of W is Coset of W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V holds the carrier of W is Coset of W
let W be Subspace of V; ::_thesis: the carrier of W is Coset of W
 the carrier of W = (0. V) + W by Lm2;
hence  the carrier of W is Coset of W by Def5; ::_thesis: verum
end;

theorem :: RUSUB_1:69
for V being RealUnitarySpace holds the carrier of V is Coset of (Omega). V
proof
let V be RealUnitarySpace; ::_thesis: the carrier of V is Coset of (Omega). V
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 = the VECTOR of V + ((Omega). V) by Th40;
hence  the carrier of V is Coset of (Omega). V by Def5; ::_thesis: verum
end;

theorem :: RUSUB_1:70
for V being RealUnitarySpace
for V1 being Subset of V st V1 is Coset of (Omega). V holds
V1 = the carrier of V
proof
let V be RealUnitarySpace; ::_thesis: for V1 being Subset of V st V1 is Coset of (Omega). V holds
V1 = the carrier of V
let V1 be Subset of V; ::_thesis: ( V1 is Coset of (Omega). V implies V1 = the carrier of V )
assume  V1 is Coset of (Omega). V ; ::_thesis: V1 = the carrier of V
then  ex v being VECTOR of V st V1 = v + ((Omega). V) by Def5;
hence  V1 = the carrier of V by Th40; ::_thesis: verum
end;

theorem :: RUSUB_1:71
for V being RealUnitarySpace
for W being Subspace of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
let W be Subspace of V; ::_thesis: for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
let C be Coset of W; ::_thesis: ( 0. V in C iff C = the carrier of W )
 ex v being VECTOR of V st C = v + W by Def5;
hence  ( 0. V in C iff C = the carrier of W ) by Th41; ::_thesis: verum
end;

theorem Th72: :: RUSUB_1:72
for V being RealUnitarySpace
for W being Subspace of V
for C being Coset of W
for u being VECTOR of V holds
( u in C iff C = u + W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for C being Coset of W
for u being VECTOR of V holds
( u in C iff C = u + W )
let W be Subspace of V; ::_thesis: for C being Coset of W
for u being VECTOR of V holds
( u in C iff C = u + W )
let C be Coset of W; ::_thesis: for u being VECTOR of V holds
( u in C iff C = u + W )
let u be VECTOR of V; ::_thesis: ( u in C iff C = u + W )
thus  ( u in C implies C = u + W ) ::_thesis: ( C = u + W implies u in C )
proof
assume A1: u in C ; ::_thesis: C = u + W
 ex v being VECTOR of V st C = v + W by Def5;
hence  C = u + W by A1, Th48; ::_thesis: verum
end;
thus  ( C = u + W implies u in C ) by Th37; ::_thesis: verum
end;

theorem :: RUSUB_1:73
for V being RealUnitarySpace
for W being Subspace of V
for C being Coset of W
for u, v being VECTOR of V st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u + v1 = v )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for C being Coset of W
for u, v being VECTOR of V st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u + v1 = v )
let W be Subspace of V; ::_thesis: for C being Coset of W
for u, v being VECTOR of V st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u + v1 = v )
let C be Coset of W; ::_thesis: for u, v being VECTOR of V st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u + v1 = v )
let u, v be VECTOR of V; ::_thesis: ( u in C & v in C implies ex v1 being VECTOR of V st
( v1 in W & u + v1 = v ) )
assume  ( u in C & v in C ) ; ::_thesis: ex v1 being VECTOR of V st
( v1 in W & u + v1 = v )
then  ( C = u + W & C = v + W ) by Th72;
hence  ex v1 being VECTOR of V st
( v1 in W & u + v1 = v ) by Th60; ::_thesis: verum
end;

theorem :: RUSUB_1:74
for V being RealUnitarySpace
for W being Subspace of V
for C being Coset of W
for u, v being VECTOR of V st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u - v1 = v )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for C being Coset of W
for u, v being VECTOR of V st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u - v1 = v )
let W be Subspace of V; ::_thesis: for C being Coset of W
for u, v being VECTOR of V st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u - v1 = v )
let C be Coset of W; ::_thesis: for u, v being VECTOR of V st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u - v1 = v )
let u, v be VECTOR of V; ::_thesis: ( u in C & v in C implies ex v1 being VECTOR of V st
( v1 in W & u - v1 = v ) )
assume  ( u in C & v in C ) ; ::_thesis: ex v1 being VECTOR of V st
( v1 in W & u - v1 = v )
then  ( C = u + W & C = v + W ) by Th72;
hence  ex v1 being VECTOR of V st
( v1 in W & u - v1 = v ) by Th61; ::_thesis: verum
end;

theorem :: RUSUB_1:75
for V being RealUnitarySpace
for W being Subspace of V
for v1, v2 being VECTOR of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v1, v2 being VECTOR of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
let W be Subspace of V; ::_thesis: for v1, v2 being VECTOR of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
let v1, v2 be VECTOR of V; ::_thesis: ( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
thus  ( ex C being Coset of W st
( v1 in C & v2 in C ) implies v1 - v2 in W ) ::_thesis: ( v1 - v2 in W implies ex C being Coset of W st
( v1 in C & v2 in C ) )
proof
given C being Coset of W such that A1: ( v1 in C & v2 in C ) ; ::_thesis: v1 - v2 in W
 ex v being VECTOR of V st C = v + W by Def5;
hence  v1 - v2 in W by A1, Th59; ::_thesis: verum
end;
assume  v1 - v2 in W ; ::_thesis: ex C being Coset of W st
( v1 in C & v2 in C )
then consider v being 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 ; ::_thesis: ( v1 in C & v2 in C )
thus  ( v1 in C & v2 in C ) by A2; ::_thesis: verum
end;

theorem :: RUSUB_1:76
for V being RealUnitarySpace
for W being Subspace of V
for u being VECTOR of V
for B, C being Coset of W st u in B & u in C holds
B = C
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for u being VECTOR of V
for B, C being Coset of W st u in B & u in C holds
B = C
let W be Subspace of V; ::_thesis: for u being VECTOR of V
for B, C being Coset of W st u in B & u in C holds
B = C
let u be VECTOR of V; ::_thesis: for B, C being Coset of W st u in B & u in C holds
B = C
let B, C be Coset of W; ::_thesis: ( u in B & u in C implies B = C )
assume A1: ( u in B & u in C ) ; ::_thesis: B = C
 ( ex v1 being VECTOR of V st B = v1 + W & ex v2 being VECTOR of V st C = v2 + W ) by Def5;
hence  B = C by A1, Th50; ::_thesis: verum
end;