let F, G be Function; :: thesis: ( F,G are_fiberwise_equipotent implies card (dom F) = card (dom G) )
assume F,G are_fiberwise_equipotent ; :: thesis: card (dom F) = card (dom G)
then ( card (F " (rng F)) = card (G " (rng F)) & rng F = rng G ) by Th75, Th78;
hence card (dom F) = card (G " (rng G)) by RELAT_1:134
.= card (dom G) by RELAT_1:134 ;
:: thesis: verum