let A be non empty set ; :: thesis: 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); :: thesis: 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; :: thesis: ( 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; :: thesis: ( ( 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;

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); :: thesis: 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; :: thesis: ( 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; :: thesis: ( ( 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;

now :: thesis: ( ( for x being Element of A holds h . x = a * (f . x) ) implies h = (ComplexFuncExtMult A) . [a,f] )

hence
( ( for x being Element of A holds h . x = a * (f . x) ) implies h = (ComplexFuncExtMult A) . [a,f] )
; :: thesis: verumassume A1:
for x being Element of A holds h . x = a * (f . x)
; :: thesis: h = (ComplexFuncExtMult A) . [a,f]

for x being Element of A holds h . x = ((ComplexFuncExtMult A) . [a,f]) . x

end;for x being Element of A holds h . x = ((ComplexFuncExtMult A) . [a,f]) . x

proof

hence
h = (ComplexFuncExtMult A) . [a,f]
by FUNCT_2:63; :: thesis: verum
let x be Element of A; :: thesis: h . x = ((ComplexFuncExtMult A) . [a,f]) . x

thus h . x = a * (f . x) by A1

.= ((ComplexFuncExtMult A) . [a,f]) . x by Def3 ; :: thesis: verum

end;thus h . x = a * (f . x) by A1

.= ((ComplexFuncExtMult A) . [a,f]) . x by Def3 ; :: thesis: verum