let p be Element of NAT ; :: thesis: for F, G being finite strict Group st card F = p & card G = p & p is prime holds
F,G are_isomorphic
let F, G be finite strict Group; :: thesis: ( card F = p & card G = p & p is prime implies F,G are_isomorphic )
assume that
A1: ( card F = p & card G = p ) and
A2: p is prime ; :: thesis: F,G are_isomorphic
( F is cyclic Group & G is cyclic Group ) by A1, A2, GR_CY_1:21;
hence F,G are_isomorphic by A1, Th23; :: thesis: verum