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: 0. UNITSTR(# D,d1,A,M,S #) = 0. V by A2;
A7: 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:72;
A8: 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:72;
A9: 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:72; :: thesis: verum

end;

( UNITSTR(# D,d1,A,M,S #) is RealUnitarySpace-like & UNITSTR(# D,d1,A,M,S #) is RealLinearSpace-like & 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 AV = the addF of V;
set MV = the Mult of V;
set SV = the scalar of V;
A10: 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 A7
.= y1 + x1
.= y + x by A7 ; :: thesis: verum

end;

A11: 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 A7
.= (x1 + y1) + z1 by A7
.= x1 + (y1 + z1) by RLVECT_1:def 6
.= the addF of V . [x1,(y + z)] by A7
.= x + (y + z) by A7 ; :: thesis: verum

end;

A12: 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, A7
.= x by RLVECT_1:10 ; :: thesis: verum

end;

A13: 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
A14: x1 + v = 0. V by ALGSTR_0:def 11;
v = - x1 by A14, RLVECT_1:def 11
.= (- 1) * x1 by RLVECT_1:29
.= (- 1) * x by A8 ;
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, A7, A14; :: thesis: verum

end;

A15: 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)
reconsider a = a as Real by XREAL_0:def 1;
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;
a * (x + y) = the Mult of V . [a,(x + y)] by A1, A4, FUNCT_1:72
.= a * (x1 + y1) by A7
.= (a * x1) + (a * y1) by RLVECT_1:def 9
.= the addF of V . [(the Mult of V . [a,x1]),(a * y)] by A8
.= the addF of V . [(a * x),(a * y)] by A8
.= (a * x) + (a * y) by A1, A3, FUNCT_1:72 ;
hence a * (x + y) = (a * x) + (a * y) ; :: thesis: verum

end;

A16: 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)
reconsider a = a, b = b as Real by XREAL_0:def 1;
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;
(a + b) * x = (a + b) * y by A8
.= (a * y) + (b * y) by RLVECT_1:def 9
.= the addF of V . [(the Mult of V . [a,y]),(b * x)] by A8
.= the addF of V . [(a * x),(b * x)] by A8
.= (a * x) + (b * x) by A1, A3, FUNCT_1:72 ;
hence (a + b) * x = (a * x) + (b * x) ; :: thesis: verum

end;

A17: 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)
reconsider a = a, b = b as Real by XREAL_0:def 1;
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;
(a * b) * x = (a * b) * y by A8
.= a * (b * y) by RLVECT_1:def 9
.= the Mult of V . [a,(b * x)] by A8
.= a * (b * x) by A1, A4, FUNCT_1:72 ;
hence (a * b) * x = a * (b * x) ; :: thesis: verum

end;

A18: 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 A8
.= x by RLVECT_1:def 9 ; :: thesis: verum

end;

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) )
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) )
reconsider x1 = x as VECTOR of V by A1, TARSKI:def 3;
reconsider y1 = y as VECTOR of V by A1, TARSKI:def 3;
reconsider z1 = z as VECTOR of V by A1, TARSKI:def 3;
A19: ( 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 A9;
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;

( 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 A9; :: thesis: verum

end;

hence ( x .|. x = 0 iff x = 0. UNITSTR(# D,d1,A,M,S #) ) by A19; :: thesis: ( 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
thus 0 <= x .|. x :: thesis: ( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

proof

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 A9; :: thesis: verum

end;

thus x .|. y = y .|. x :: thesis: ( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

proof

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 A9;
hence x .|. y = y .|. x by A9; :: thesis: verum

end;

thus (x + y) .|. z = (x .|. z) + (y .|. z) :: thesis: (a * x) .|. y = a * (x .|. y)

proof

A20: the scalar of V . [y1,z1] = y1 .|. z1 by BHSP_1:def 1;
A21: (x + y) .|. z = the scalar of V . [(x + y),z] by A9
.= the scalar of V . [(x1 + y1),z] by A7
.= (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 A9
.= (the scalar of V . [x,z]) + (the scalar of V . [y,z]) by A9
.= (x1 .|. z1) + (y1 .|. z1) by A20, BHSP_1:def 1 ;
hence (x + y) .|. z = (x .|. z) + (y .|. z) by A21; :: thesis: verum

end;

thus (a * x) .|. y = a * (x .|. y) :: thesis: verum

proof

A22: (a * x) .|. y = the scalar of V . [(a * x),y] by A9
.= the scalar of V . [(a * x1),y] by A8
.= (a * x1) .|. y1 by BHSP_1:def 1
.= a * (x1 .|. y1) by BHSP_1:def 2 ;
a * (x .|. y) = a * (the scalar of V . [x,y]) by A9
.= a * (x1 .|. y1) by BHSP_1:def 1 ;
hence (a * x) .|. y = a * (x .|. y) by A22; :: thesis: verum

end;

end;

hence ( UNITSTR(# D,d1,A,M,S #) is RealUnitarySpace-like & UNITSTR(# D,d1,A,M,S #) is RealLinearSpace-like & 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 A10, A11, A12, A13, A15, A16, A17, A18, BHSP_1:def 2, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 9; :: thesis: verum

end;

hence UNITSTR(# D,d1,A,M,S #) is Subspace of V by A1, A3, A4, A5, A6, Def1; :: thesis: verum

end;

hence UNITSTR(# D,d1,A,M,S #) is Subspace of V ; :: thesis: verum