let C be non empty strict CLSStruct ; ( 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
; ( 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; RLVECT_1:def 2 ( 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; RLVECT_1:def 3 ( 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
RLVECT_1:def 4 ( 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 is right_complementable
ALGSTR_0:def 16 ( C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )
thus
for a being Complex
for u, v being VECTOR of C holds a * (u + v) = (a * u) + (a * v)
by Lm2, A1; CLVECT_1:def 2 ( 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; CLVECT_1:def 3 ( 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; CLVECT_1:def 4 C is scalar-unital
thus
for v being Element of C holds 1r * v = v
by Th12, A1; CLVECT_1:def 5 verum