:: deftheorem defines ComplexVectSpace CFUNCDOM:def 6 :
for A being non empty set holds ComplexVectSpace A = CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #);