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 and
A2: card G = p and
A3: p is prime ; :: thesis: F,G are_isomorphic
A4: F is cyclic Group by A1, A3, GR_CY_1:45;
G is cyclic Group by A2, A3, GR_CY_1:45;
hence F,G are_isomorphic by A1, A2, A4, Th23; :: thesis: verum