theorem Th22: :: PRE_POLY:23

for F being Function
for X being set holds Card (F | X) = (Card F) | X