theorem Th48: :: CARD_FIN:49

for X9 being set
for F being Function holds
( dom (Intersect (F,((dom F) --> X9))) = dom F & ( for x being set st x in dom F holds
(Intersect (F,((dom F) --> X9))) . x = (F . x) /\ X9 ) )