let G, H be Group; :: thesis: for g being Homomorphism of G,H holds card (Image g) c= card G
let g be Homomorphism of G,H; :: thesis: card (Image g) c= card G
card (g .: the carrier of G) c= card the carrier of G by CARD_1:67;
hence card (Image g) c= card G by Def10; :: thesis: verum