let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL
for r1, r2 being Real holds r1 (#) (r2 (#) f) = (r1 * r2) (#) f
let f be PartFunc of X,ExtREAL; :: thesis: for r1, r2 being Real holds r1 (#) (r2 (#) f) = (r1 * r2) (#) f
let r1, r2 be Real; :: thesis: r1 (#) (r2 (#) f) = (r1 * r2) (#) f
A1: dom (r1 (#) (r2 (#) f)) = dom (r2 (#) f) by MESFUNC1:def 6;
then A2: dom (r1 (#) (r2 (#) f)) = dom f by MESFUNC1:def 6;
A3: dom ((r1 * r2) (#) f) = dom f by MESFUNC1:def 6;
for x being Element of X st x in dom (r1 (#) (r2 (#) f)) holds
(r1 (#) (r2 (#) f)) . x = ((r1 * r2) (#) f) . x
proof
let x be Element of X; :: thesis: ( x in dom (r1 (#) (r2 (#) f)) implies (r1 (#) (r2 (#) f)) . x = ((r1 * r2) (#) f) . x )
assume A4: x in dom (r1 (#) (r2 (#) f)) ; :: thesis: (r1 (#) (r2 (#) f)) . x = ((r1 * r2) (#) f) . x
then (r1 (#) (r2 (#) f)) . x = r1 * ((r2 (#) f) . x) by MESFUNC1:def 6;
then A5: (r1 (#) (r2 (#) f)) . x = r1 * (r2 * (f . x)) by A1, A4, MESFUNC1:def 6;
((r1 * r2) (#) f) . x = (r1 * r2) * (f . x) by A2, A3, A4, MESFUNC1:def 6;
hence (r1 (#) (r2 (#) f)) . x = ((r1 * r2) (#) f) . x by A5, XXREAL_3:66; :: thesis: verum
end;
hence r1 (#) (r2 (#) f) = (r1 * r2) (#) f by A2, A3, PARTFUN1:5; :: thesis: verum