let A be non empty Subset of REAL; :: thesis: for r being Real
for f being PartFunc of REAL,REAL st A c= dom f holds
(r (#) f) | A = r (#) (f | A)
let r be Real; :: thesis: for f being PartFunc of REAL,REAL st A c= dom f holds
(r (#) f) | A = r (#) (f | A)
let f be PartFunc of REAL,REAL; :: thesis: ( A c= dom f implies (r (#) f) | A = r (#) (f | A) )
assume AA: A c= dom f ; :: thesis: (r (#) f) | A = r (#) (f | A)
then A1: A c= dom (r (#) f) by VALUED_1:def 5;
set F = (r (#) f) | A;
set g = r (#) (f | A);
A2: dom (r (#) (f | A)) = dom (f | A) by VALUED_1:def 5
.= A by RELAT_1:62, AA ;
for x being object st x in dom ((r (#) f) | A) holds
((r (#) f) | A) . x = (r (#) (f | A)) . x

proof

let x be object ; :: thesis: ( x in dom ((r (#) f) | A) implies ((r (#) f) | A) . x = (r (#) (f | A)) . x )
assume D1: x in dom ((r (#) f) | A) ; :: thesis: ((r (#) f) | A) . x = (r (#) (f | A)) . x
then reconsider x = x as Real ;
((r (#) f) | A) . x = (r (#) f) . x by FUNCT_1:49, D1
.= r * (f . x) by VALUED_1:6
.= r * ((f | A) . x) by FUNCT_1:49, D1
.= (r (#) (f | A)) . x by VALUED_1:6 ;
hence ((r (#) f) | A) . x = (r (#) (f | A)) . x ; :: thesis: verum

end;

hence (r (#) f) | A = r (#) (f | A) by FUNCT_1:2, A1, A2, RELAT_1:62; :: thesis: verum