let G, H be Group; :: thesis: ( G,H are_isomorphic & G is finite implies H is finite )
assume that
A1: G,H are_isomorphic and
A2: G is finite ; :: thesis: H is finite
consider h being Homomorphism of G,H such that
A3: h is bijective by A1, Def15;
h is onto by A3;
then A4: rng h = the carrier of H by FUNCT_2:def 3;
the carrier of G is finite by A2;
then dom h is finite ;
then the carrier of H is finite by A4, FINSET_1:26;
hence H is finite ; :: thesis: verum