let X, Y be set ; :: thesis: ( X,Y are_equipotent & X is finite implies Y is finite )
assume X,Y are_equipotent ; :: thesis: ( not X is finite or Y is finite )
then consider f being Function such that
A1: ( f is one-to-one & dom f = X & rng f = Y ) by WELLORD2:def 4;
given p being Function such that A2: rng p = X and
A3: dom p in omega ; :: according to FINSET_1:def 1 :: thesis: Y is finite
take f * p ; :: according to FINSET_1:def 1 :: thesis: ( rng (f * p) = Y & dom (f * p) in omega )
thus rng (f * p) = Y by A1, A2, RELAT_1:47; :: thesis: dom (f * p) in omega
thus dom (f * p) in omega by A1, A2, A3, RELAT_1:46; :: thesis: verum