let p be Prime; :: thesis: 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
let G be finite commutative Group; :: thesis: 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
let H, H1, H2 be Subgroup of G; :: thesis: ( H1 is p -commutative-group & H2 is p -commutative-group & the carrier of H = H1 * H2 implies H is p -commutative-group )
assume that
A1: ( H1 is p -commutative-group & H2 is p -commutative-group ) and
A2: the carrier of H = H1 * H2 ; :: thesis: H is p -commutative-group
H is p -group by A1, A2, Th19;
hence H is p -commutative-group ; :: thesis: verum