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
f is one-to-one and
A1: dom f = X and
A2: rng f = Y ;
given p being Function such that A3: rng p = X and
A4: 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, A3, RELAT_1:28; :: thesis: dom (f * p) in omega
thus dom (f * p) in omega by A1, A3, A4, RELAT_1:27; :: thesis: verum