let Omega be non empty set ; :: thesis: for f, g being PartFunc of Omega,REAL holds (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g)
let f, g be PartFunc of Omega,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
.= dom (f (#) g) by VALUED_1:def 4 ;

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

let x be object ; :: thesis: ( x in dom ((R_EAL f) (#) (R_EAL g)) implies ((R_EAL f) (#) (R_EAL g)) . x = (f (#) g) . x )
assume A2: x in dom ((R_EAL f) (#) (R_EAL g)) ; :: thesis: ((R_EAL f) (#) (R_EAL g)) . x = (f (#) g) . x
hence ((R_EAL f) (#) (R_EAL g)) . x = ((R_EAL f) . x) * ((R_EAL g) . x) by MESFUNC1:def 5
.= (f . x) * (g . x) by EXTREAL1:1
.= (f (#) g) . x by A1, A2, VALUED_1:def 4 ;
:: thesis: verum

end;

hence (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) by A1, FUNCT_1:2; :: thesis: verum