let V be ComplexLinearSpace; :: thesis:
let V1 be Subset of V; :: thesis:
let D be non empty set ; :: thesis:
let d1 be Element of D; :: thesis:
let A be BinOp of D; :: thesis:
let M be Function of [:COMPLEX,D:],D; :: thesis:
assume that
A1: V1 = D and
A2: d1 = 0. V and
A3: A = the addF of V || V1 and
A4: M = the Mult of V | [:COMPLEX,V1:] ; :: thesis:
set W = CLSStruct(# D,d1,A,M #);
A5: for x, y being VECTOR of CLSStruct(# D,d1,A,M #) holds x + y = the addF of V . [x,y] by A1, A3, FUNCT_1:49;
A6: ( CLSStruct(# D,d1,A,M #) is Abelian & CLSStruct(# D,d1,A,M #) is add-associative & CLSStruct(# D,d1,A,M #) is right_zeroed & CLSStruct(# D,d1,A,M #) is right_complementable & CLSStruct(# D,d1,A,M #) is vector-distributive & CLSStruct(# D,d1,A,M #) is scalar-distributive & CLSStruct(# D,d1,A,M #) is scalar-associative & CLSStruct(# D,d1,A,M #) is scalar-unital )

set MV = the Mult of V;
set AV = the addF of V;
thus for x, y being VECTOR of CLSStruct(# D,d1,A,M #) holds x + y = y + x :: according to RLVECT_1:def 2 :: thesis:

let x, y be VECTOR of CLSStruct(# D,d1,A,M #); :: thesis:
reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;
thus x + y = x1 + y1 by A5
.= y1 + x1
.= y + x by A5 ; :: thesis:

end;

thus for x, y, z being VECTOR of CLSStruct(# D,d1,A,M #) holds (x + y) + z = x + (y + z) :: according to RLVECT_1:def 3 :: thesis:

let x, y, z be VECTOR of CLSStruct(# D,d1,A,M #); :: thesis:
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1, TARSKI:def 3;
thus (x + y) + z = the addF of V . [(x + y),z1] by A5
.= (x1 + y1) + z1 by A5
.= x1 + (y1 + z1) by RLVECT_1:def 3
.= the addF of V . [x1,(y + z)] by A5
.= x + (y + z) by A5 ; :: thesis:

end;

thus for x being VECTOR of CLSStruct(# D,d1,A,M #) holds x + (0. CLSStruct(# D,d1,A,M #)) = x :: according to RLVECT_1:def 4 :: thesis:

let x be VECTOR of CLSStruct(# D,d1,A,M #); :: thesis:
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
thus x + (0. CLSStruct(# D,d1,A,M #)) = y + (0. V) by A2, A5
.= x by RLVECT_1:4 ; :: thesis:

end;

let x be VECTOR of CLSStruct(# D,d1,A,M #); :: according to ALGSTR_0:def 16 :: thesis:
reconsider x1 = x as VECTOR of V by A1, TARSKI:def 3;
consider v being VECTOR of V such that
A7: x1 + v = 0. V by ALGSTR_0:def 11;
reconsider mj = - 1r as Element of COMPLEX by XCMPLX_0:def 2;
v = - x1 by A7, RLVECT_1:def 10
.= (- 1r) * x1 by Th3
.= the Mult of V . [mj,x]
.= (- 1r) * x by A1, A4, FUNCT_1:49 ;
then reconsider y = v as VECTOR of CLSStruct(# D,d1,A,M #) ;
take y ; :: according to ALGSTR_0:def 11 :: thesis:
thus x + y = 0. CLSStruct(# D,d1,A,M #) by A2, A5, A7; :: thesis:

end;

thus for z being Complex
for x, y being VECTOR of CLSStruct(# D,d1,A,M #) holds z * (x + y) = (z * x) + (z * y) :: according to CLVECT_1:def 2 :: thesis:

let z be Complex; :: thesis:
let x, y be VECTOR of CLSStruct(# D,d1,A,M #); :: thesis:
reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;
A8: ( z * x1 = z * x & z * y1 = z * y ) by A1, A4, Lm4;
thus z * (x + y) = z * (x1 + y1) by A1, A4, A5, Lm4
.= (z * x1) + (z * y1) by Def2
.= (z * x) + (z * y) by A5, A8 ; :: thesis:

end;

thus for z1, z2 being Complex
for x being VECTOR of CLSStruct(# D,d1,A,M #) holds (z1 + z2) * x = (z1 * x) + (z2 * x) :: according to CLVECT_1:def 3 :: thesis:

let z1, z2 be Complex; :: thesis:
let x be VECTOR of CLSStruct(# D,d1,A,M #); :: thesis:
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
A9: ( z1 * y = z1 * x & z2 * y = z2 * x ) by A1, A4, Lm4;
thus (z1 + z2) * x = (z1 + z2) * y by A1, A4, Lm4
.= (z1 * y) + (z2 * y) by Def3
.= (z1 * x) + (z2 * x) by A5, A9 ; :: thesis:

end;

thus for z1, z2 being Complex
for x being VECTOR of CLSStruct(# D,d1,A,M #) holds (z1 * z2) * x = z1 * (z2 * x) :: according to CLVECT_1:def 4 :: thesis:

let z1, z2 be Complex; :: thesis:
let x be VECTOR of CLSStruct(# D,d1,A,M #); :: thesis:
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
A10: z2 * y = z2 * x by A1, A4, Lm4;
thus (z1 * z2) * x = (z1 * z2) * y by A1, A4, Lm4
.= z1 * (z2 * y) by Def4
.= z1 * (z2 * x) by A1, A4, A10, Lm4 ; :: thesis:

end;

let x be VECTOR of CLSStruct(# D,d1,A,M #); :: according to CLVECT_1:def 5 :: thesis:
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
thus 1r * x = 1r * y by A1, A4, Lm4
.= x by Def5 ; :: thesis:

end;

0. CLSStruct(# D,d1,A,M #) = 0. V by A2;
hence CLSStruct(# D,d1,A,M #) is Subspace of V by A1, A3, A4, A6, Def8; :: thesis: