let A be non empty set ; :: thesis: for f, g, h being Element of Funcs (A,COMPLEX) holds
( h = () . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )

let f, g, h be Element of Funcs (A,COMPLEX); :: thesis: ( h = () . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )
A1: now :: thesis: ( ( for x being Element of A holds h . x = (f . x) * (g . x) ) implies h = () . (f,g) )
assume A2: for x being Element of A holds h . x = (f . x) * (g . x) ; :: thesis: h = () . (f,g)
now :: thesis: for x being Element of A holds (() . (f,g)) . x = h . x
let x be Element of A; :: thesis: (() . (f,g)) . x = h . x
A3: x in dom (multcomplex .: (f,g)) by Lm1;
thus (() . (f,g)) . x = (multcomplex .: (f,g)) . x by Def2
.= multcomplex . ((f . x),(g . x)) by
.= (f . x) * (g . x) by BINOP_2:def 5
.= h . x by A2 ; :: thesis: verum
end;
hence h = () . (f,g) by FUNCT_2:63; :: thesis: verum
end;
now :: thesis: ( h = () . (f,g) implies for x being Element of A holds h . x = (f . x) * (g . x) )
assume A4: h = () . (f,g) ; :: thesis: for x being Element of A holds h . x = (f . x) * (g . x)
let x be Element of A; :: thesis: h . x = (f . x) * (g . x)
A5: x in dom (multcomplex .: (f,g)) by Lm1;
thus h . x = (multcomplex .: (f,g)) . x by
.= multcomplex . ((f . x),(g . x)) by
.= (f . x) * (g . x) by BINOP_2:def 5 ; :: thesis: verum
end;
hence ( h = () . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) ) by A1; :: thesis: verum