let A be non empty set ; :: thesis: for f, g being Element of Funcs (A,REAL) holds (RealFuncMult A) . (f,g) = f (#) g
let f, g be Element of Funcs (A,REAL); :: thesis: (RealFuncMult A) . (f,g) = f (#) g
A1: dom ((RealFuncMult A) . (f,g)) = A by FUNCT_2:def 1;
a1: dom (f (#) g) = (dom f) /\ (dom g) by VALUED_1:def 4
.= A /\ (dom g) by FUNCT_2:def 1
.= A /\ A by FUNCT_2:def 1
.= A ;

now :: thesis: for x being object st x in dom (f (#) g) holds
((RealFuncMult A) . (f,g)) . x = (f (#) g) . x

let x be object ; :: thesis: ( x in dom (f (#) g) implies ((RealFuncMult A) . (f,g)) . x = (f (#) g) . x )
assume a0: x in dom (f (#) g) ; :: thesis: ((RealFuncMult A) . (f,g)) . x = (f (#) g) . 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 a1, a0, A3, FUNCOP_1:22
.= (f . x) * (g . x) by BINOP_2:def 11
.= (f (#) g) . x by VALUED_1:5 ; :: thesis: verum

end;

hence (RealFuncMult A) . (f,g) = f (#) g by A1, a1, FUNCT_1:2; :: thesis: verum