let A be non empty set ; for f, h being Element of Funcs (A,COMPLEX)
for a being Complex holds
( h = (ComplexFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
let f, h be Element of Funcs (A,COMPLEX); for a being Complex holds
( h = (ComplexFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
let a be Complex; ( h = (ComplexFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
thus
( h = (ComplexFuncExtMult A) . [a,f] implies for x being Element of A holds h . x = a * (f . x) )
by Def3; ( ( for x being Element of A holds h . x = a * (f . x) ) implies h = (ComplexFuncExtMult A) . [a,f] )
reconsider a = a as Element of COMPLEX by XCMPLX_0:def 2;
hence
( ( for x being Element of A holds h . x = a * (f . x) ) implies h = (ComplexFuncExtMult A) . [a,f] )
; verum