set W = CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #);
( CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is Abelian & CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is add-associative & CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_zeroed & CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_complementable & CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is ComplexLinearSpace-like )

proof

thus for v, w being VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds v + w = w + v :: according to RLVECT_1:def 5 :: thesis: ( CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is add-associative & CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_zeroed & CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_complementable & CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is ComplexLinearSpace-like )

proof

let v, w be VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #); :: thesis: v + w = w + v
reconsider v' = v, w' = w as VECTOR of V ;
v + w = v' + w' ;
hence v + w = w' + v'
.= w + v ;
:: thesis: verum

end;

thus for u, v, w being VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds (u + v) + w = u + (v + w) :: according to RLVECT_1:def 6 :: thesis: ( CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_zeroed & CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_complementable & CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is ComplexLinearSpace-like )

proof

let u, v, w be VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #); :: thesis: (u + v) + w = u + (v + w)
reconsider u' = u, v' = v, w' = w as VECTOR of V ;
(u' + v') + w' = u' + (v' + w') by RLVECT_1:def 6;
hence (u + v) + w = u + (v + w) ; :: thesis: verum

end;

thus for v being VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds v + (0. CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #)) = v :: according to RLVECT_1:def 7 :: thesis: ( CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_complementable & CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is ComplexLinearSpace-like )

proof

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

end;

for v being VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds v is right_complementable

proof

let v be VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #); :: thesis: v is right_complementable
reconsider v' = v as VECTOR of V ;
v' is right_complementable by ALGSTR_0:def 16;
then consider w' being VECTOR of V such that
A2: v' + w' = 0. V by ALGSTR_0:def 11;
reconsider w = w' as VECTOR of CLSStruct(# the carrier of V,the U2 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 U2 of V,the addF of V,the Mult of V #)
thus v + w = 0. CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) by A2; :: thesis: verum

end;

hence CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_complementable by ALGSTR_0:def 16; :: thesis: CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is ComplexLinearSpace-like
thus for a being Complex
for v, w being VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds a * (v + w) = (a * v) + (a * w) :: according to CLVECT_1:def 2 :: thesis: ( ( for b₁, b₂ being Element of COMPLEX
for b₃ being Element of the carrier of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds (b₁ + b₂) * b₃ = (b₁ * b₃) + (b₂ * b₃) ) & ( for b₁, b₂ being Element of COMPLEX
for b₃ being Element of the carrier of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) ) & ( for b₁ being Element of the carrier of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds 1r * b₁ = b₁ ) )

proof

let a be Complex; :: thesis: for v, w being VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #); :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider v' = v, w' = w as VECTOR of V ;
a * (v' + w') = (a * v') + (a * w') by CLVECT_1:def 2;
hence a * (v + w) = (a * v) + (a * w) ; :: thesis: verum

end;

thus for a, b being Complex
for v being VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds (a + b) * v = (a * v) + (b * v) :: thesis: ( ( for b₁, b₂ being Element of COMPLEX
for b₃ being Element of the carrier of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) ) & ( for b₁ being Element of the carrier of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds 1r * b₁ = b₁ ) )

proof

let a, b be Complex; :: thesis: for v being VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v' = v as VECTOR of V ;
(a + b) * v' = (a * v') + (b * v') by CLVECT_1:def 2;
hence (a + b) * v = (a * v) + (b * v) ; :: thesis: verum

end;

thus for a, b being Complex
for v being VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds (a * b) * v = a * (b * v) :: thesis: for b₁ being Element of the carrier of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds 1r * b₁ = b₁

proof

let a, b be Complex; :: thesis: for v being VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds (a * b) * v = a * (b * v)
let v be VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #); :: thesis: (a * b) * v = a * (b * v)
reconsider v' = v as VECTOR of V ;
(a * b) * v' = a * (b * v') by CLVECT_1:def 2;
hence (a * b) * v = a * (b * v) ; :: thesis: verum

end;

thus for v being VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds 1r * v = v :: thesis: verum

proof

let v be VECTOR of CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #); :: thesis: 1r * v = v
reconsider v' = v as VECTOR of V ;
thus 1r * v = 1r * v'
.= v by CLVECT_1:def 2 ; :: thesis: verum

end;

end;

then reconsider W = CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) as ComplexLinearSpace ;
W is Subspace of V

proof

thus ( the carrier of W c= the carrier of V & 0. W = 0. V ) ; :: according to CLVECT_1:def 5 :: thesis: ( the addF of W = K306(the addF of V,the carrier of W) & the Mult of W = the Mult of V | [:COMPLEX ,the carrier of W:] )
thus ( the addF of W = K306(the addF of V,the carrier of W) & the Mult of W = the Mult of V | [:COMPLEX ,the carrier of W:] ) by RELSET_1:34; :: thesis: verum

end;

hence CLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is strict Subspace of V ; :: thesis: verum