let X be non empty set ; :: thesis: for A being set
for r being Real
for f being PartFunc of X,ExtREAL holds (r (#) f) | A = r (#) (f | A)
let A be set ; :: thesis: for r being Real
for f being PartFunc of X,ExtREAL holds (r (#) f) | A = r (#) (f | A)
let r be Real; :: thesis: for f being PartFunc of X,ExtREAL holds (r (#) f) | A = r (#) (f | A)
let f be PartFunc of X,ExtREAL; :: thesis: (r (#) f) | A = r (#) (f | A)
A1: dom (r (#) f) = dom f by MESFUNC1:def 6;
then A2: dom ((r (#) f) | A) = (dom f) /\ A by RELAT_1:61;
then A3: dom ((r (#) f) | A) = dom (f | A) by RELAT_1:61;
then A4: dom ((r (#) f) | A) = dom (r (#) (f | A)) by MESFUNC1:def 6;

now :: thesis: for x being Element of X st x in dom ((r (#) f) | A) holds
((r (#) f) | A) . x = (r (#) (f | A)) . x

let x be Element of X; :: thesis: ( x in dom ((r (#) f) | A) implies ((r (#) f) | A) . x = (r (#) (f | A)) . x )
assume B1: x in dom ((r (#) f) | A) ; :: thesis: ((r (#) f) | A) . x = (r (#) (f | A)) . x
then B2: x in dom f by A2, XBOOLE_0:def 4;
((r (#) f) | A) . x = (r (#) f) . x by B1, FUNCT_1:47;
then ((r (#) f) | A) . x = r * (f . x) by B2, A1, MESFUNC1:def 6;
then ((r (#) f) | A) . x = r * ((f | A) . x) by B1, A3, FUNCT_1:47;
hence ((r (#) f) | A) . x = (r (#) (f | A)) . x by B1, A4, MESFUNC1:def 6; :: thesis: verum

end;

hence (r (#) f) | A = r (#) (f | A) by A4, PARTFUN1:5; :: thesis: verum