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:72;
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:72; :: 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:72;
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 11 ; :: 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 10
.= the Mult of V . [a,(b * x)] by A6
.= a * (b * x) by A1, A4, FUNCT_1:72 ;
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:72
.= a * (x1 + y1) by A8
.= (a * x1) + (a * y1) by RLVECT_1:def 8
.= 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:72 ;
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:10 ; :: 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 9
.= 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:72 ;
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 13
.= (- 1) * x1 by RLVECT_1:29
.= (- 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 6
.= 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 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8, RLVECT_1:def 9, RLVECT_1:def 10, RLVECT_1:def 11; :: 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