let p be natural prime number ; :: thesis: for G, H being strict Group st G,H are_isomorphic & G is p -commutative-group holds
H is p -commutative-group
let G, H be strict Group; :: thesis: ( G,H are_isomorphic & G is p -commutative-group implies H is p -commutative-group )
assume that
A1: G,H are_isomorphic and
A2: G is p -commutative-group ; :: thesis: H is p -commutative-group
A3: H is p -group by A1, A2, Th22;
H is p -commutative-group-like by A1, A2, Th33;
hence H is p -commutative-group by A3; :: thesis: verum