set W = UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #);
A1: for u, v, w being VECTOR of holds (u + v) + w = u + (v + w)

proof

let u, v, w be VECTOR of ; :: thesis: (u + v) + w = u + (v + w)
reconsider u' = u, v' = v, w' = w as VECTOR of ;
thus (u + v) + w = (u' + v') + w'
.= u' + (v' + w') by RLVECT_1:def 6
.= u + (v + w) ; :: thesis: verum

end;

A2: for v being VECTOR of holds v + (0. UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #)) = v

proof

let v be VECTOR of ; :: thesis: v + (0. UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #)) = v
reconsider v' = v as VECTOR of ;
thus v + (0. UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #)) = v' + (0. V)
.= v by RLVECT_1:10 ; :: thesis: verum

end;

A3: UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) is right_complementable

proof

let v be VECTOR of ; :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider v' = v as VECTOR of ;
consider w' being VECTOR of such that
A4: v' + w' = 0. V by ALGSTR_0:def 11;
reconsider w = w' as VECTOR of ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #)
thus v + w = 0. UNITSTR(# the carrier of V,the U2 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 holds 1 * v = v

proof

let v be VECTOR of ; :: thesis: 1 * v = v
reconsider v' = v as VECTOR of ;
thus 1 * v = 1 * v'
.= v by RLVECT_1:def 9 ; :: thesis: verum

end;

A6: for a, b being real number
for v being VECTOR of holds (a + b) * v = (a * v) + (b * v)

proof

let a, b be real number ; :: thesis: for v being VECTOR of holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of ; :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v' = v as VECTOR of ;
thus (a + b) * v = (a + b) * v'
.= (a * v') + (b * v') by RLVECT_1:def 9
.= (a * v) + (b * v) ; :: thesis: verum

end;

A7: for a being real number
for v, w being VECTOR of holds a * (v + w) = (a * v) + (a * w)

proof

let a be real number ; :: thesis: for v, w being VECTOR of holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of ; :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider v' = v, w' = w as VECTOR of ;
thus a * (v + w) = a * (v' + w')
.= (a * v') + (a * w') by RLVECT_1:def 9
.= (a * v) + (a * w) ; :: thesis: verum

end;

A8: now

let a be Real; :: thesis: for v, w being VECTOR of
for v', w' being VECTOR of st v = v' & w = w' holds
( v + w = v' + w' & a * v = a * v' & v .|. w = v' .|. w' )
let v, w be VECTOR of ; :: thesis: for v', w' being VECTOR of st v = v' & w = w' holds
( v + w = v' + w' & a * v = a * v' & v .|. w = v' .|. w' )
let v', w' be VECTOR of ; :: thesis: ( v = v' & w = w' implies ( v + w = v' + w' & a * v = a * v' & v .|. w = v' .|. w' ) )
assume that
A9: v = v' and
A10: w = w' ; :: thesis: ( v + w = v' + w' & a * v = a * v' & v .|. w = v' .|. w' )
thus v + w = v' + w' by A9, A10; :: thesis: ( a * v = a * v' & v .|. w = v' .|. w' )
thus a * v = a * v' by A9; :: thesis: v .|. w = v' .|. w'
thus v .|. w = the scalar of UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) . [v,w] by BHSP_1:def 1
.= v' .|. w' by A9, A10, BHSP_1:def 1 ; :: thesis: verum

end;

A11: for v, w being VECTOR of holds v + w = w + v

proof

let v, w be VECTOR of ; :: thesis: v + w = w + v
reconsider v' = v, w' = w as VECTOR of ;
thus v + w = w' + v' by A8
.= w + v ; :: thesis: verum

end;

A12: 0. UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = 0. V ;
A13: for x, y, z being VECTOR of
for a being Real holds
( ( x .|. x = 0 implies x = 0. UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) ) & ( x = 0. UNITSTR(# the carrier of V,the U2 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 ; :: thesis: for a being Real holds
( ( x .|. x = 0 implies x = 0. UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) ) & ( x = 0. UNITSTR(# the carrier of V,the U2 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 U2 of V,the addF of V,the Mult of V,the scalar of V #) ) & ( x = 0. UNITSTR(# the carrier of V,the U2 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 x' = x as VECTOR of ;
reconsider y' = y as VECTOR of ;
reconsider z' = z as VECTOR of ;
A14: (x + y) .|. z = (x' + y') .|. z' by A8
.= (x' .|. z') + (y' .|. z') by BHSP_1:def 2 ;
x' .|. x' = x .|. x by A8;
hence ( x .|. x = 0 iff x = 0. UNITSTR(# the carrier of V,the U2 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) )
x' .|. x' = 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) )
x' .|. y' = 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) )
x' .|. z' = 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 * x') .|. y' by A8
.= a * (x' .|. y') 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 holds (a * b) * v = a * (b * v)

proof

let a, b be real number ; :: thesis: for v being VECTOR of holds (a * b) * v = a * (b * v)
let v be VECTOR of ; :: thesis: (a * b) * v = a * (b * v)
reconsider v' = v as VECTOR of ;
thus (a * b) * v = (a * b) * v'
.= a * (b * v') by RLVECT_1:def 9
.= a * (b * v) ; :: thesis: verum

end;

then reconsider W = UNITSTR(# the carrier of V,the U2 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 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 9;
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:34;
( 0. W = 0. V & the Mult of W = the Mult of V | [:REAL ,the carrier of W:] ) by RELSET_1:34;
hence UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) is strict Subspace of V by A15, Def1; :: thesis: verum