theorem Th3: :: FUNCOP_1:3

for f being Function
for A being set holds (f | A) ~ = (f ~) | A