let Gc, Hc be finite strict cyclic Group; :: thesis: ( card Hc = card Gc implies Hc,Gc are_isomorphic )
set p = card Hc;
assume card Hc = card Gc ; :: thesis: Hc,Gc are_isomorphic
then A1: INT.Group (card Hc),Gc are_isomorphic by Th15;
INT.Group (card Hc),Hc are_isomorphic by Th15;
hence Hc,Gc are_isomorphic by A1, GROUP_6:67; :: thesis: verum