let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for r being Real holds R_EAL (r (#) f) = r (#) (R_EAL f)
let f be PartFunc of X,REAL; :: thesis: for r being Real holds R_EAL (r (#) f) = r (#) (R_EAL f)
let r be Real; :: thesis: R_EAL (r (#) f) = r (#) (R_EAL f)
dom (R_EAL (r (#) f)) = dom (R_EAL f) by VALUED_1:def 5;
then A1: dom (R_EAL (r (#) f)) = dom (r (#) (R_EAL f)) by MESFUNC1:def 6;

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

let x be object ; :: thesis: ( x in dom (R_EAL (r (#) f)) implies (R_EAL (r (#) f)) . x = (r (#) (R_EAL f)) . x )
reconsider rr = r as R_eal by XXREAL_0:def 1;
assume A2: x in dom (R_EAL (r (#) f)) ; :: thesis: (R_EAL (r (#) f)) . x = (r (#) (R_EAL f)) . x
then (R_EAL (r (#) f)) . x = r * (f . x) by VALUED_1:def 5;
then (R_EAL (r (#) f)) . x = rr * (f . x) by EXTREAL1:1;
hence (R_EAL (r (#) f)) . x = (r (#) (R_EAL f)) . x by A1, A2, MESFUNC1:def 6; :: thesis: verum

end;

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