theorem Th47: :: FUNCT_1:48

for X being set
for x being object
for f being Function st x in (dom f) /\ X holds
(f | X) . x = f . x