let X be non empty set ; :: thesis: for Y being set
for f being PartFunc of X,ExtREAL
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let Y be set ; :: thesis: for f being PartFunc of X,ExtREAL
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let f be PartFunc of X,ExtREAL; :: thesis: for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let r be Real; :: thesis: (r (#) f) | Y = r (#) (f | Y)

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

let x be Element of X; :: thesis: ( x in dom ((r (#) f) | Y) implies ((r (#) f) | Y) . x = (r (#) (f | Y)) . x )
assume A2: x in dom ((r (#) f) | Y) ; :: thesis: ((r (#) f) | Y) . x = (r (#) (f | Y)) . x
then A3: x in (dom (r (#) f)) /\ Y by RELAT_1:61;
then A4: x in Y by XBOOLE_0:def 4;
A5: x in dom (r (#) f) by A3, XBOOLE_0:def 4;
then x in dom f by MESFUNC1:def 6;
then x in (dom f) /\ Y by A4, XBOOLE_0:def 4;
then A6: x in dom (f | Y) by RELAT_1:61;
then A7: x in dom (r (#) (f | Y)) by MESFUNC1:def 6;
thus ((r (#) f) | Y) . x = (r (#) f) . x by A2, FUNCT_1:47
.= r * (f . x) by A5, MESFUNC1:def 6
.= r * ((f | Y) . x) by A6, FUNCT_1:47
.= (r (#) (f | Y)) . x by A7, MESFUNC1:def 6 ; :: thesis: verum

end;

dom ((r (#) f) | Y) = (dom (r (#) f)) /\ Y by RELAT_1:61
.= (dom f) /\ Y by MESFUNC1:def 6
.= dom (f | Y) by RELAT_1:61
.= dom (r (#) (f | Y)) by MESFUNC1:def 6 ;
hence (r (#) f) | Y = r (#) (f | Y) by A1, PARTFUN1:5; :: thesis: verum