let X be non empty set ; :: thesis: for Y being set
for f being PartFunc of X,COMPLEX
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let Y be set ; :: thesis: for f being PartFunc of X,COMPLEX
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let f be PartFunc of X,COMPLEX ; :: thesis: for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let r be Real; :: thesis: (r (#) f) | Y = r (#) (f | Y)
B1: dom ((r (#) f) | Y) = (dom (r (#) f)) /\ Y by RELAT_1:90;
then dom ((r (#) f) | Y) = (dom f) /\ Y by VALUED_1:def 5;
then B2: dom ((r (#) f) | Y) = dom (f | Y) by RELAT_1:90;
then B3: dom ((r (#) f) | Y) = dom (r (#) (f | Y)) by VALUED_1:def 5;

now

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) & x in Y ) by B1, XBOOLE_0:def 4;
thus ((r (#) f) | Y) . x = (r (#) f) . x by A2, FUNCT_1:70
.= r * (f . x) by A3, VALUED_1:def 5
.= r * ((f | Y) . x) by A2, B2, FUNCT_1:70
.= (r (#) (f | Y)) . x by A2, B3, VALUED_1:def 5 ; :: thesis: verum

end;

hence (r (#) f) | Y = r (#) (f | Y) by B3, PARTFUN1:34; :: thesis: verum