theorem :: GROUPP_1:32

for p being Prime
for G being finite Group
for N1, N2 being normal Subgroup of G st N2 is Subgroup of center G & N1 is p -commutative-group & N2 is p -commutative-group holds
ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N is p -commutative-group )