let p be Prime; :: thesis: for G being finite commutative Group
for H, H1, H2 being Subgroup of G st H1 is p -group & H2 is p -group & the carrier of H = H1 * H2 holds
H is p -group
let G be finite commutative Group; :: thesis: for H, H1, H2 being Subgroup of G st H1 is p -group & H2 is p -group & the carrier of H = H1 * H2 holds
H is p -group
let H, H1, H2 be Subgroup of G; :: thesis: ( H1 is p -group & H2 is p -group & the carrier of H = H1 * H2 implies H is p -group )
assume that
A1: ( H1 is p -group & H2 is p -group ) and
A2: the carrier of H = H1 * H2 ; :: thesis: H is p -group
for a being Element of H holds a is p -power

proof

let a be Element of H; :: thesis: a is p -power
a in H1 * H2 by A2;
then consider b1, b2 being Element of G such that
A3: ( a = b1 * b2 & b1 in H1 & b2 in H2 ) by GROUP_11:6;
( b1 is p -power & b2 is p -power ) by A1, A3, Th15;
then consider r being Nat such that
A4: ord (b1 * b2) = p |^ r by Def1;
ord a = p |^ r by A3, A4, GROUP_8:5;
hence a is p -power ; :: thesis: verum

end;

hence H is p -group by Th17; :: thesis: verum