theorem :: CLASSES1:81

for F, G being Function st F,G are_fiberwise_equipotent holds
card (dom F) = card (dom G)