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)
P1: 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

let x be set ; :: thesis: ( x in dom ((R_EAL f) (#) (R_EAL g)) implies ((R_EAL f) (#) (R_EAL g)) . x = (f (#) g) . x )
assume AS: x in dom ((R_EAL f) (#) (R_EAL g)) ; :: thesis: ((R_EAL f) (#) (R_EAL g)) . x = (f (#) g) . x
thus ((R_EAL f) (#) (R_EAL g)) . x = ((R_EAL f) . x) * ((R_EAL g) . x) by AS, MESFUNC1:def 5
.= (f . x) * (g . x) by EXTREAL1:13
.= (f (#) g) . x by VALUED_1:def 4, AS, P1 ; :: thesis: verum

end;

hence (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) by FUNCT_1:9, P1; :: thesis: verum