let G be finite Group; :: thesis: for H being Group
for g being Homomorphism of G,H holds card (Image g) <= card G
let H be Group; :: thesis: for g being Homomorphism of G,H holds card (Image g) <= card G
let g be Homomorphism of G,H; :: thesis: card (Image g) <= card G
Segm (card (Image g)) c= Segm (card G) by Th52;
hence card (Image g) <= card G by NAT_1:39; :: thesis: verum