theorem Th43: :: CLVECT_1:43

for V being ComplexLinearSpace
for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX,V1:] holds
CLSStruct(# D,d1,A,M #) is Subspace of V