let G, H 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 g .: the carrier of G is finite ;
hence Image g is finite by Def10; :: thesis: verum