let X be non empty set ; :: thesis: for f, g being PartFunc of X,REAL holds (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g)
let f, g be PartFunc of X,REAL ; :: thesis: (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g)
A1: dom ((R_EAL f) (#) (R_EAL g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) by MESFUNC1:def 5;
then A4: dom ((R_EAL f) (#) (R_EAL g)) = dom (R_EAL (f (#) g)) by VALUED_1:def 4;

now

let x be Element of X; :: thesis: ( x in dom ((R_EAL f) (#) (R_EAL g)) implies ((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x )
assume A2: x in dom ((R_EAL f) (#) (R_EAL g)) ; :: thesis: ((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x
then A3: ((R_EAL f) (#) (R_EAL g)) . x = ((R_EAL f) . x) * ((R_EAL g) . x) by MESFUNC1:def 5;
x in dom (f (#) g) by A1, A2, VALUED_1:def 4;
then (f (#) g) . x = (f . x) * (g . x) by VALUED_1:def 4;
hence ((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x by A3, EXTREAL1:13; :: thesis: verum

end;

hence (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) by A4, PARTFUN1:34; :: thesis: verum