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

( h = (ComplexFuncMult A) . (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 = (ComplexFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )

( h = (ComplexFuncMult A) . (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 = (ComplexFuncMult A) . (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 = (ComplexFuncMult A) . (f,g) )

assume A2:
for x being Element of A holds h . x = (f . x) * (g . x)
; :: thesis: h = (ComplexFuncMult A) . (f,g)

end;now :: thesis: for x being Element of A holds ((ComplexFuncMult A) . (f,g)) . x = h . x

hence
h = (ComplexFuncMult A) . (f,g)
by FUNCT_2:63; :: thesis: verumlet x be Element of A; :: thesis: ((ComplexFuncMult A) . (f,g)) . x = h . x

A3: x in dom (multcomplex .: (f,g)) by Lm1;

thus ((ComplexFuncMult A) . (f,g)) . x = (multcomplex .: (f,g)) . x by Def2

.= multcomplex . ((f . x),(g . x)) by A3, FUNCOP_1:22

.= (f . x) * (g . x) by BINOP_2:def 5

.= h . x by A2 ; :: thesis: verum

end;A3: x in dom (multcomplex .: (f,g)) by Lm1;

thus ((ComplexFuncMult A) . (f,g)) . x = (multcomplex .: (f,g)) . x by Def2

.= multcomplex . ((f . x),(g . x)) by A3, FUNCOP_1:22

.= (f . x) * (g . x) by BINOP_2:def 5

.= h . x by A2 ; :: thesis: verum

now :: thesis: ( h = (ComplexFuncMult A) . (f,g) implies for x being Element of A holds h . x = (f . x) * (g . x) )

hence
( h = (ComplexFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )
by A1; :: thesis: verumassume A4:
h = (ComplexFuncMult A) . (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 A4, Def2

.= multcomplex . ((f . x),(g . x)) by A5, FUNCOP_1:22

.= (f . x) * (g . x) by BINOP_2:def 5 ; :: thesis: verum

end;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 A4, Def2

.= multcomplex . ((f . x),(g . x)) by A5, FUNCOP_1:22

.= (f . x) * (g . x) by BINOP_2:def 5 ; :: thesis: verum