let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for E being set holds (R_EAL f) | E = R_EAL (f | E)
let f be PartFunc of X,REAL; :: thesis: for E being set holds (R_EAL f) | E = R_EAL (f | E)
let E be set ; :: thesis: (R_EAL f) | E = R_EAL (f | E)
dom (R_EAL (f | E)) = dom (f | E) by MESFUNC5:def 7;
then A1: dom ((R_EAL f) | E) = dom (R_EAL (f | E)) by MESFUNC5:def 7;

now :: thesis: for x being Element of X st x in dom ((R_EAL f) | E) holds
((R_EAL f) | E) . x = (R_EAL (f | E)) . x

let x be Element of X; :: thesis: ( x in dom ((R_EAL f) | E) implies ((R_EAL f) | E) . x = (R_EAL (f | E)) . x )
assume x in dom ((R_EAL f) | E) ; :: thesis: ((R_EAL f) | E) . x = (R_EAL (f | E)) . x
(R_EAL (f | E)) . x = (f | E) . x by MESFUNC5:def 7;
hence ((R_EAL f) | E) . x = (R_EAL (f | E)) . x by MESFUNC5:def 7; :: thesis: verum

end;

hence (R_EAL f) | E = R_EAL (f | E) by A1, PARTFUN1:5; :: thesis: verum