let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for Y being set
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let f be PartFunc of X,REAL; :: thesis: for Y being set
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let Y be set ; :: thesis: for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let r be Real; :: thesis: (r (#) f) | Y = r (#) (f | Y)
A1: dom ((r (#) f) | Y) = (dom (r (#) f)) /\ Y by RELAT_1:61
.= (dom f) /\ Y by VALUED_1:def 5
.= dom (f | Y) by RELAT_1:61 ;
A2: dom ((r (#) f) | Y) c= dom (r (#) f) by RELAT_1:60;
A3: 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 A4: x in dom ((r (#) f) | Y) ; :: thesis: (r (#) (f | Y)) . x = ((r (#) f) | Y) . x
then x in dom (r (#) (f | Y)) by A1, VALUED_1:def 5;
then (r (#) (f | Y)) . x = r * ((f | Y) . x) by VALUED_1:def 5;
then (r (#) (f | Y)) . x = r * (f . x) by A1, A4, FUNCT_1:47;
then (r (#) (f | Y)) . x = (r (#) f) . x by A2, A4, VALUED_1:def 5;
hence (r (#) (f | Y)) . x = ((r (#) f) | Y) . x by A4, FUNCT_1:47; :: thesis: verum
end;
dom ((r (#) f) | Y) = dom (r (#) (f | Y)) by A1, VALUED_1:def 5;
hence (r (#) f) | Y = r (#) (f | Y) by A3, PARTFUN1:5; :: thesis: verum