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

proof

let u, v, w be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult 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 CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds v + (0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v

proof

let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: v + (0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v
reconsider v9 = v as VECTOR of V ;
thus v + (0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v9 + (0. V)
.= v by RLVECT_1:4 ; :: thesis: verum

end;

A3: CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_complementable

proof

let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult 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 CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
thus v + w = 0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by A4; :: thesis: verum

end;

A5: for z1, z2 being Complex
for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (z1 * z2) * v = z1 * (z2 * v)

proof

let z1, z2 be Complex; :: thesis: for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (z1 * z2) * v = z1 * (z2 * v)
let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: (z1 * z2) * v = z1 * (z2 * v)
reconsider v9 = v as VECTOR of V ;
thus (z1 * z2) * v = (z1 * z2) * v9
.= z1 * (z2 * v9) by Def4
.= z1 * (z2 * v) ; :: thesis: verum

end;

A6: for z1, z2 being Complex
for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (z1 + z2) * v = (z1 * v) + (z2 * v)

proof

let z1, z2 be Complex; :: thesis: for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (z1 + z2) * v = (z1 * v) + (z2 * v)
let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: (z1 + z2) * v = (z1 * v) + (z2 * v)
reconsider v9 = v as VECTOR of V ;
thus (z1 + z2) * v = (z1 + z2) * v9
.= (z1 * v9) + (z2 * v9) by Def3
.= (z1 * v) + (z2 * v) ; :: thesis: verum

end;

A7: for z being Complex
for v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds z * (v + w) = (z * v) + (z * w)

proof

let z be Complex; :: thesis: for v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds z * (v + w) = (z * v) + (z * w)
let v, w be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: z * (v + w) = (z * v) + (z * w)
reconsider v9 = v, w9 = w as VECTOR of V ;
thus z * (v + w) = z * (v9 + w9)
.= (z * v9) + (z * w9) by Def2
.= (z * v) + (z * w) ; :: thesis: verum

end;

A8: for z being Complex
for v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
for v9, w9 being VECTOR of V st v = v9 & w = w9 holds
( v + w = v9 + w9 & z * v = z * v9 ) ;
A9: for v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds v + w = w + v

proof

let v, w be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult 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;

for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds 1r * v = v

proof

let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: 1r * v = v
reconsider v9 = v as VECTOR of V ;
thus 1r * v = 1r * v9
.= v by Def5 ; :: thesis: verum

end;

then reconsider W = CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) as ComplexLinearSpace by A9, A1, A2, A3, A7, A6, A5, Def2, Def3, Def4, Def5, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4;
A10: the Mult of W = the Mult of V | [:COMPLEX, the carrier of W:] by RELSET_1:19;
( 0. W = 0. V & the addF of W = the addF of V || the carrier of W ) by RELSET_1:19;
hence CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V by A10, Def8; :: thesis: verum