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;

A2: now :: thesis: for x being Element of X st x in dom ((R_EAL f) (#) (R_EAL g)) holds
((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x

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 A3: x in dom ((R_EAL f) (#) (R_EAL g)) ; :: thesis: ((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x
then x in dom (f (#) g) by A1, VALUED_1:def 4;
then A4: (f (#) g) . x = (f . x) * (g . x) by VALUED_1:def 4
.= (f . x) * (g . x) ;
((R_EAL f) (#) (R_EAL g)) . x = ((R_EAL f) . x) * ((R_EAL g) . x) by A3, MESFUNC1:def 5;
hence ((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x by A4; :: thesis: verum

end;

dom ((R_EAL f) (#) (R_EAL g)) = dom (R_EAL (f (#) g)) by A1, VALUED_1:def 4;
hence (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) by A2, PARTFUN1:5; :: thesis: verum