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, Th17; :: thesis: verum

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, Th17; :: thesis: verum