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 by Def15;
consider g1 being Homomorphism of H,G such that
A3: g1 is bijective by A1, Def15;
Image g1 = G by A3, Th67;
then A4: card G c= card H by Th61;
Image h = H by A2, Th67;
then card H c= card G by Th61;
hence card G = card H by A4, XBOOLE_0:def 10; :: thesis: verum