theorem Th78: :: CLASSES1:78

for F, G being Function holds
( F,G are_fiberwise_equipotent iff for X being set holds card (F " X) = card (G " X) )