theorem Th16: :: MESFUN15:14

for X being non empty set
for f being PartFunc of X,REAL
for E being set holds (R_EAL f) | E = R_EAL (f | E)