theorem Th10: :: CLOPBAN1:10

for X being non empty set
for Y being ComplexLinearSpace holds CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is ComplexLinearSpace