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

X0: now

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 x = v, y = u, z = w, yx = u + v, xz = v + w, ax = a * v, az = a * w, bx = b * v as Element of C_LinComb V ;
( @ x = v & @ y = u & @ z = w & @ yx = u + v & @ xz = v + w & @ ax = a * v & @ az = a * w & @ bx = b * v ) ;
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 ;

A1: now

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 )
assume A2: ( v = K & u = L ) ; :: thesis: v + u = K + L
( @ (@ K) = K & @ (@ L) = L ) ;
hence v + u = K + L by A2, Def9; :: thesis: verum

end;

A4: now

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 Def10;
hence a * v = a * L ; :: thesis: verum

end;

thus v + w = K + M by A1
.= w + v by A1 ; :: 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 A1
.= (L + K) + M by A1
.= L + (K + M) by Th61
.= L + KM by A1
.= u + (v + w) by A1 ; :: 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 A1
.= v by Th62 ; :: 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 Def8;
then - K in CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) by STRUCT_0:def 5;
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 A1
.= 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) by Th82 ;
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 )
thus a * (v + w) = a * KM by A4
.= a * (K + M) by A1
.= (a * K) + (a * M) by Th69
.= aK + (a * M) by A4
.= aK + aM by A4
.= (a * v) + (a * w) by A1 ; :: thesis: ( (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )
thus (a + b) * v = (a + b) * K by A4
.= (a * K) + (b * K) by Th68
.= aK + (b * K) by A4
.= aK + bK by A4
.= (a * v) + (b * v) by A1 ; :: thesis: ( (a * b) * v = a * (b * v) & 1r * v = v )
thus (a * b) * v = (a * b) * K by A4
.= a * (b * K) by Th70
.= a * bK by A4
.= a * (b * v) by A4 ; :: thesis: 1r * v = v
thus 1r * v = 1r * K by A4
.= v by Th71 ; :: thesis: verum

end;

then X1: ( ( for v, w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds v + w = w + v ) & ( 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) ) & ( for v being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v ) & ( for v being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult 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) #) ) & ( for a being Complex
for v, w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds a * (v + w) = (a * v) + (a * w) ) & ( for a, b being Complex
for v being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds (a + b) * v = (a * v) + (b * v) ) & ( for a, b being Complex
for v being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds (a * b) * v = a * (b * v) ) & ( for v being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds 1r * v = v ) ) ;

now

let v be Element of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #); :: thesis: v is right_complementable
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) #) by X0;
hence v is right_complementable by ALGSTR_0:def 11; :: thesis: verum

end;

hence CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) is ComplexLinearSpace by X1, ALGSTR_0:def 16, CLVECT_1:def 2, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7; :: thesis: verum