let A be non empty Subset of REAL; :: thesis: for r being Real
for f being Function of REAL,REAL holds (r (#) f) | A = r (#) (f | A)
let r be Real; :: thesis: for f being Function of REAL,REAL holds (r (#) f) | A = r (#) (f | A)
let f be Function of REAL,REAL; :: thesis: (r (#) f) | A = r (#) (f | A)
set F = (r (#) f) | A;
set g = r (#) (f | A);
A1: dom ((r (#) f) | A) = A by FUNCT_2:def 1;
A2: dom (r (#) (f | A)) = A by FUNCT_2:def 1;
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; :: thesis: verum