set S = CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #);

A1: now :: thesis: for a, b being Complex
for v, u, w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds
( v + w = w + v & (u + v) + w = u + (v + w) & v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v & ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )

let a, b be Complex; :: thesis: for v, u, w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds
( v + w = w + v & (u + v) + w = u + (v + w) & v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v & ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )
let v, u, w be VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #); :: thesis: ( v + w = w + v & (u + v) + w = u + (v + w) & v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v & ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )
reconsider a1 = a, b1 = b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider x = v, y = u, z = w, yx = u + v, xz = v + w, ax = a1 * v, az = a1 * w, bx = b1 * v as Element of C_LinComb V ;
A2: ( @ z = w & @ yx = u + v ) ;
A3: ( @ xz = v + w & @ ax = a * v ) ;
A4: ( @ az = a * w & @ bx = b * v ) ;
( @ x = v & @ y = u ) ;
then reconsider K = v, L = u, M = w, LK = u + v, KM = v + w, aK = a * v, aM = a * w, bK = b * v as C_Linear_Combination of V by A2, A3, A4;

A5: now :: thesis: for v, u being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)
for K, L being C_Linear_Combination of V st v = K & u = L holds
v + u = K + L

let v, u be VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #); :: thesis: for K, L being C_Linear_Combination of V st v = K & u = L holds
v + u = K + L
let K, L be C_Linear_Combination of V; :: thesis: ( v = K & u = L implies v + u = K + L )
A6: ( @ (@ K) = K & @ (@ L) = L ) ;
assume ( v = K & u = L ) ; :: thesis: v + u = K + L
hence v + u = K + L by A6, Def15; :: thesis: verum

end;

hence v + w = K + M
.= w + v by A5 ;
:: thesis: ( (u + v) + w = u + (v + w) & v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v & ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )
thus (u + v) + w = LK + M by A5
.= (L + K) + M by A5
.= L + (K + M) by Th22
.= L + KM by A5
.= u + (v + w) by A5 ; :: thesis: ( v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v & ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )
thus v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = K + (ZeroCLC V) by A5
.= v by Th23 ; :: thesis: ( ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )
- K in the carrier of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) by Def12;
then - K in CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) ;
then - K = vector (CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #),(- K)) by RLVECT_2:def 1;
then v + (vector (CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #),(- K))) = K - K by A5
.= 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) by Th37 ;
hence ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) ; :: thesis: ( a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )

A7: now :: thesis: for v being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)
for L being C_Linear_Combination of V
for a being Complex st v = L holds
a * v = a * L

let v be VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #); :: thesis: for L being C_Linear_Combination of V
for a being Complex st v = L holds
a * v = a * L
let L be C_Linear_Combination of V; :: thesis: for a being Complex st v = L holds
a * v = a * L
let a be Complex; :: thesis: ( v = L implies a * v = a * L )
assume v = L ; :: thesis: a * v = a * L
then (C_LCMult V) . [a,v] = a * (@ (@ L)) by Def16;
hence a * v = a * L ; :: thesis: verum

end;

hence a * (v + w) = a1 * KM
.= a1 * (K + M) by A5
.= (a1 * K) + (a1 * M) by Th28
.= aK + (a1 * M) by A7
.= aK + aM by A7
.= (a * v) + (a * w) by A5 ;
:: thesis: ( (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )
thus (a + b) * v = (a1 + b1) * K by A7
.= (a1 * K) + (b1 * K) by Th27
.= aK + (b * K) by A7
.= aK + bK by A7
.= (a * v) + (b * v) by A5 ; :: thesis: ( (a * b) * v = a * (b * v) & 1r * v = v )
thus (a * b) * v = (a * b) * K by A7
.= a1 * (b1 * K) by Th29
.= a * bK by A7
.= a * (b * v) by A7 ; :: thesis: 1r * v = v
thus 1r * v = 1r * K by A7
.= v by Th30 ; :: thesis: verum

end;

A8: for v being Element of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds v is right_complementable by A1;
for u, v, w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds (u + v) + w = u + (v + w) by A1;
hence CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) is ComplexLinearSpace by A1, A8, ALGSTR_0:def 16, CLVECT_1:def 2, CLVECT_1:def 3, CLVECT_1:def 4, CLVECT_1:def 5, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: verum