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;
rng h = the carrier of H by A3, FUNCT_2:def 3;
hence H is finite by A2; :: thesis: verum