let C be non empty strict CLSStruct ; :: thesis: ( C = ComplexVectSpace A implies ( C is Abelian & C is add-associative & C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital ) )

assume A1: C = ComplexVectSpace A ; :: thesis: ( C is Abelian & C is add-associative & C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )

thus for u, v being Element of C holds u + v = v + u by Th5, A1; :: according to RLVECT_1:def 2 :: thesis: ( C is add-associative & C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )

thus for u, v, w being Element of C holds (u + v) + w = u + (v + w) by Th6, A1; :: according to RLVECT_1:def 3 :: thesis: ( C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )

thus for u being Element of C holds u + (0. C) = u :: according to RLVECT_1:def 4 :: thesis: ( C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )

for u, v being VECTOR of C holds a * (u + v) = (a * u) + (a * v) by Lm2, A1; :: according to CLVECT_1:def 2 :: thesis: ( C is scalar-distributive & C is scalar-associative & C is scalar-unital )

thus for a, b being Complex

for v being VECTOR of C holds (a + b) * v = (a * v) + (b * v) by Th14, A1; :: according to CLVECT_1:def 3 :: thesis: ( C is scalar-associative & C is scalar-unital )

thus for a, b being Complex

for v being VECTOR of C holds (a * b) * v = a * (b * v) by Th13, A1; :: according to CLVECT_1:def 4 :: thesis: C is scalar-unital

thus for v being Element of C holds 1r * v = v by Th12, A1; :: according to CLVECT_1:def 5 :: thesis: verum

assume A1: C = ComplexVectSpace A ; :: thesis: ( C is Abelian & C is add-associative & C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )

thus for u, v being Element of C holds u + v = v + u by Th5, A1; :: according to RLVECT_1:def 2 :: thesis: ( C is add-associative & C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )

thus for u, v, w being Element of C holds (u + v) + w = u + (v + w) by Th6, A1; :: according to RLVECT_1:def 3 :: thesis: ( C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )

thus for u being Element of C holds u + (0. C) = u :: according to RLVECT_1:def 4 :: thesis: ( C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )

proof

thus
for u being Element of C holds u is right_complementable
:: according to ALGSTR_0:def 16 :: thesis: ( C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )
let u be Element of C; :: thesis: u + (0. C) = u

reconsider v = u as Element of Funcs (A,COMPLEX) by A1;

thus u + (0. C) = (ComplexFuncAdd A) . ((ComplexFuncZero A),v) by Th5, A1

.= u by Th10 ; :: thesis: verum

end;reconsider v = u as Element of Funcs (A,COMPLEX) by A1;

thus u + (0. C) = (ComplexFuncAdd A) . ((ComplexFuncZero A),v) by Th5, A1

.= u by Th10 ; :: thesis: verum

proof

thus
for a being Complex
let u be Element of C; :: thesis: u is right_complementable

reconsider v = u as Element of Funcs (A,COMPLEX) by A1;

reconsider mj = - 1r as Element of COMPLEX by XCMPLX_0:def 2;

reconsider w = (ComplexFuncExtMult A) . [mj,v] as VECTOR of C by A1;

take w ; :: according to ALGSTR_0:def 11 :: thesis: u + w = 0. C

thus u + w = 0. C by Th11, A1; :: thesis: verum

end;reconsider v = u as Element of Funcs (A,COMPLEX) by A1;

reconsider mj = - 1r as Element of COMPLEX by XCMPLX_0:def 2;

reconsider w = (ComplexFuncExtMult A) . [mj,v] as VECTOR of C by A1;

take w ; :: according to ALGSTR_0:def 11 :: thesis: u + w = 0. C

thus u + w = 0. C by Th11, A1; :: thesis: verum

for u, v being VECTOR of C holds a * (u + v) = (a * u) + (a * v) by Lm2, A1; :: according to CLVECT_1:def 2 :: thesis: ( C is scalar-distributive & C is scalar-associative & C is scalar-unital )

thus for a, b being Complex

for v being VECTOR of C holds (a + b) * v = (a * v) + (b * v) by Th14, A1; :: according to CLVECT_1:def 3 :: thesis: ( C is scalar-associative & C is scalar-unital )

thus for a, b being Complex

for v being VECTOR of C holds (a * b) * v = a * (b * v) by Th13, A1; :: according to CLVECT_1:def 4 :: thesis: C is scalar-unital

thus for v being Element of C holds 1r * v = v by Th12, A1; :: according to CLVECT_1:def 5 :: thesis: verum