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