let l be CLSStruct ; :: thesis: ( CLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is ComplexLinearSpace implies l is ComplexLinearSpace )
assume A1: CLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is ComplexLinearSpace ; :: thesis: l is ComplexLinearSpace
reconsider l = l as non empty CLSStruct by A1;
reconsider l0 = CLSStruct(# the carrier of l,(0. l), the addF of l, the Mult of l #) as ComplexLinearSpace by A1;
A2: l is Abelian

proof

let v, w be VECTOR of l; :: according to RLVECT_1:def 2 :: thesis: v + w = w + v
reconsider v1 = v as VECTOR of l0 ;
reconsider w1 = w as VECTOR of l0 ;
thus v + w = v1 + w1
.= w1 + v1
.= w + v ; :: thesis: verum

end;

A3: l is add-associative

proof

let u, v, w be VECTOR of l; :: according to RLVECT_1:def 3 :: thesis: (u + v) + w = u + (v + w)
reconsider u1 = u as VECTOR of l0 ;
reconsider v1 = v as VECTOR of l0 ;
reconsider w1 = w as VECTOR of l0 ;
thus (u + v) + w = (u1 + v1) + w1
.= u1 + (v1 + w1) by RLVECT_1:def 3
.= u + (v + w) ; :: thesis: verum

end;

A4: ( l is vector-distributive & l is scalar-distributive & l is scalar-associative & l is scalar-unital )

proof

thus for z being Complex
for v, w being VECTOR of l holds z * (v + w) = (z * v) + (z * w) :: according to CLVECT_1:def 2 :: thesis: ( l is scalar-distributive & l is scalar-associative & l is scalar-unital )

proof

let z be Complex; :: thesis: for v, w being VECTOR of l holds z * (v + w) = (z * v) + (z * w)
let v, w be VECTOR of l; :: thesis: z * (v + w) = (z * v) + (z * w)
reconsider v1 = v, w1 = w as VECTOR of l0 ;
thus z * (v + w) = z * (v1 + w1)
.= (z * v1) + (z * w1) by CLVECT_1:def 2
.= (z * v) + (z * w) ; :: thesis: verum

end;

thus for z1, z2 being Complex
for v being VECTOR of l holds (z1 + z2) * v = (z1 * v) + (z2 * v) :: according to CLVECT_1:def 3 :: thesis: ( l is scalar-associative & l is scalar-unital )

proof

let z1, z2 be Complex; :: thesis: for v being VECTOR of l holds (z1 + z2) * v = (z1 * v) + (z2 * v)
let v be VECTOR of l; :: thesis: (z1 + z2) * v = (z1 * v) + (z2 * v)
reconsider v1 = v as VECTOR of l0 ;
thus (z1 + z2) * v = (z1 + z2) * v1
.= (z1 * v1) + (z2 * v1) by CLVECT_1:def 3
.= (z1 * v) + (z2 * v) ; :: thesis: verum

end;

thus for z1, z2 being Complex
for v being VECTOR of l holds (z1 * z2) * v = z1 * (z2 * v) :: according to CLVECT_1:def 4 :: thesis: l is scalar-unital

proof

let z1, z2 be Complex; :: thesis: for v being VECTOR of l holds (z1 * z2) * v = z1 * (z2 * v)
let v be VECTOR of l; :: thesis: (z1 * z2) * v = z1 * (z2 * v)
reconsider v1 = v as VECTOR of l0 ;
thus (z1 * z2) * v = (z1 * z2) * v1
.= z1 * (z2 * v1) by CLVECT_1:def 4
.= z1 * (z2 * v) ; :: thesis: verum

end;

let v be VECTOR of l; :: according to CLVECT_1:def 5 :: thesis: 1r * v = v
reconsider v1 = v as VECTOR of l0 ;
thus 1r * v = 1r * v1
.= v by CLVECT_1:def 5 ; :: thesis: verum

end;

A5: l is right_complementable

proof

let v be VECTOR of l; :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider v1 = v as VECTOR of l0 ;
consider w1 being VECTOR of l0 such that
A6: v1 + w1 = 0. l0 by ALGSTR_0:def 11;
reconsider w = w1 as VECTOR of l ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. l
thus v + w = 0. l by A6; :: thesis: verum

end;

l is right_zeroed

proof

let v be VECTOR of l; :: according to RLVECT_1:def 4 :: thesis: v + (0. l) = v
reconsider v1 = v as VECTOR of l0 ;
thus v + (0. l) = v1 + (0. l0)
.= v by RLVECT_1:def 4 ; :: thesis: verum

end;

hence l is ComplexLinearSpace by A2, A3, A5, A4; :: thesis: verum