for p being prime Nat
for G being finite commutative Group
for H, H1, H2 being Subgroup of G st H1 is p -commutative-group & H2 is p -commutative-group & the carrier of H = H1 * H2 holds
H is p -commutative-group