let A be non empty set ; CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is ComplexLinearSpace
set IT = CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #);
A1:
for u, v, w being VECTOR of holds (u + v) + w = u + (v + w)
by Th8;
A2:
for u being VECTOR of holds u is right_complementable
proof
let u be
VECTOR of ;
u is right_complementable
reconsider u' =
u as
Element of
Funcs A,
COMPLEX ;
reconsider w =
(ComplexFuncExtMult A) . [(- 1r ),u'] as
VECTOR of ;
take
w
;
ALGSTR_0:def 11 u + w = 0. CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #)
thus
u + w = 0. CLSStruct(#
(Funcs A,COMPLEX ),
(ComplexFuncZero A),
(ComplexFuncAdd A),
(ComplexFuncExtMult A) #)
by Th13;
verum
end;
A3:
for u being VECTOR of holds u + (0. CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #)) = u
proof
let u be
VECTOR of ;
u + (0. CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #)) = u
reconsider u' =
u as
Element of
Funcs A,
COMPLEX ;
thus u + (0. CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #)) =
(ComplexFuncAdd A) . (ComplexFuncZero A),
u'
by Th7
.=
u
by Th12
;
verum
end;
A4:
for a, b being Complex
for v being VECTOR of holds (a + b) * v = (a * v) + (b * v)
by Th16;
A5:
for a being Complex
for u, v being VECTOR of holds a * (u + v) = (a * u) + (a * v)
by Lm2;
A6:
for v being VECTOR of holds 1r * v = v
by Th14;
A7:
for a, b being Complex
for v being VECTOR of holds (a * b) * v = a * (b * v)
by Th15;
for u, v being VECTOR of holds u + v = v + u
by Th7;
hence
CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is ComplexLinearSpace
by A1, A3, A2, A5, A4, A7, A6, ALGSTR_0:def 16, CLVECT_1:def 2, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7; verum