let F, G be Function; :: thesis: ( F,G are_fiberwise_equipotent implies card (dom F) = card (dom G) )
assume A1: F,G are_fiberwise_equipotent ; :: thesis: card (dom F) = card (dom G)
A2: ( card (F " (rng F)) = card (G " (rng F)) & rng F = rng G ) by A1, Th83, Th86;
thus card (dom F) = card (G " (rng G)) by A2, RELAT_1:169
.= card (dom G) by RELAT_1:169 ; :: thesis: verum