let A be non empty set ; :: thesis: for f, g, h being Element of Funcs (A,REAL) holds
( h = (RealFuncMult 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,REAL); :: thesis: ( h = (RealFuncMult 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 = (RealFuncMult A) . (f,g) )

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

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

let x be Element of A; :: thesis: ((RealFuncMult A) . (f,g)) . x = h . x
A3: dom (multreal .: (f,g)) = A by FUNCT_2:def 1;
thus ((RealFuncMult A) . (f,g)) . x = (multreal .: (f,g)) . x by Def2
.= multreal . ((f . x),(g . x)) by A3, FUNCOP_1:22
.= (f . x) * (g . x) by BINOP_2:def 11
.= h . x by A2 ; :: thesis: verum

end;

hence h = (RealFuncMult A) . (f,g) ; :: thesis: verum

end;

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

assume A4: h = (RealFuncMult 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: dom (multreal .: (f,g)) = A by FUNCT_2:def 1;
thus h . x = (multreal .: (f,g)) . x by A4, Def2
.= multreal . ((f . x),(g . x)) by A5, FUNCOP_1:22
.= (f . x) * (g . x) by BINOP_2:def 11 ; :: thesis: verum

end;

hence ( h = (RealFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) ) by A1; :: thesis: verum