let p be natural prime number ; :: thesis: for G being finite Group
for H being Subgroup of G
for a being Element of G st H is p -group & a in H holds
a is p -power
let G be finite Group; :: thesis: for H being Subgroup of G
for a being Element of G st H is p -group & a in H holds
a is p -power
let H be Subgroup of G; :: thesis: for a being Element of G st H is p -group & a in H holds
a is p -power
let a be Element of G; :: thesis: ( H is p -group & a in H implies a is p -power )
assume that
A1: H is p -group and
A2: a in H ; :: thesis: a is p -power
a is Element of H by A2, STRUCT_0:def 5;
then consider b being Element of H such that
A3: b = a ;
consider r being natural number such that
A4: ord b = p |^ r by A1, Def1;
ord a = p |^ r by A3, A4, GROUP_8:5;
hence a is p -power by Def1; :: thesis: verum