:: deftheorem Def3 defines ComplexFuncExtMult CFUNCDOM:def 3 :
for A being non empty set
for b₂ being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) holds
( b₂ = ComplexFuncExtMult A iff for z being Complex
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (b₂ . [z,f]) . x = z * (f . x) );