let p be natural prime number ; :: thesis: for G, H being strict Group st G,H are_isomorphic & G is p -group holds
H is p -group
let G, H be strict Group; :: thesis: ( G,H are_isomorphic & G is p -group implies H is p -group )
assume that
A1: G,H are_isomorphic and
A2: G is p -group ; :: thesis: H is p -group
consider r being natural number such that
A3: card G = p |^ r by A2, GROUP_10:def 17;
card H = p |^ r by A1, A3, GROUP_6:73;
hence H is p -group by GROUP_10:def 17; :: thesis: verum