let G, H be strict Group; :: thesis: ( G,H are_isomorphic implies card G = card H )
assume A1: G,H are_isomorphic ; :: thesis: card G = card H
then consider h being Homomorphism of G,H such that
A2: h is bijective ;
consider g1 being Homomorphism of H,G such that
A3: g1 is bijective by A1, Def11;
Image g1 = G by A3, Th57;
then A4: card G c= card H by Th52;
Image h = H by A2, Th57;
hence card G = card H by A4, Th52; :: thesis: verum