let H, G be Group; :: thesis: for g being Homomorphism of G,H st G is finite holds
Image g is finite
let g be Homomorphism of G,H; :: thesis: ( G is finite implies Image g is finite )
assume G is finite ; :: thesis: Image g is finite
then the carrier of G is finite ;
then g .: the carrier of G is finite ;
then the carrier of (Image g) is finite by Def11;
hence Image g is finite ; :: thesis: verum