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)

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:
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 6
.= u + (v + w) ; :: thesis:

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

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:
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:10 ; :: thesis:

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

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

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

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:
reconsider v9 = v as VECTOR of V ;
thus 1 * v = 1 * v9
.= v by RLVECT_1:def 9 ; :: thesis:

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)

let a, b be real number ; :: thesis:
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:
reconsider v9 = v as VECTOR of V ;
thus (a + b) * v = (a + b) * v9
.= (a * v9) + (b * v9) by RLVECT_1:def 9
.= (a * v) + (b * v) ; :: thesis:

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)

let a be real number ; :: thesis:
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:
reconsider v9 = v, w9 = w as VECTOR of V ;
thus a * (v + w) = a * (v9 + w9)
.= (a * v9) + (a * w9) by RLVECT_1:def 9
.= (a * v) + (a * w) ; :: thesis:

end;

let a be Real; :: thesis:
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:
let v9, w9 be VECTOR of V; :: thesis:
assume that
A9: v = v9 and
A10: w = w9 ; :: thesis:
thus v + w = v9 + w9 by A9, A10; :: thesis:
thus a * v = a * v9 by A9; :: thesis:
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:

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

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:
reconsider v9 = v, w9 = w as VECTOR of V ;
thus v + w = w9 + v9 by A8
.= w + v ; :: thesis:

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

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:
let a be Real; :: thesis:
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:
x9 .|. x9 = x .|. x by A8;
hence 0 <= x .|. x by BHSP_1:def 2; :: thesis:
x9 .|. y9 = x .|. y by A8;
hence x .|. y = y .|. x by A8; :: thesis:
x9 .|. z9 = x .|. z by A8;
hence (x + y) .|. z = (x .|. z) + (y .|. z) by A8, A14; :: thesis:
(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:

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)

let a, b be real number ; :: thesis:
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:
reconsider v9 = v as VECTOR of V ;
thus (a * b) * v = (a * b) * v9
.= a * (b * v9) by RLVECT_1:def 9
.= a * (b * v) ; :: thesis:

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 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 ZeroF of V,the addF of V,the Mult of V,the scalar of V #) is strict Subspace of V by A15, Def1; :: thesis: