let p be prime Nat; :: 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;
then consider b being Element of H such that
A3: b = a ;
consider r being Nat 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 ; :: thesis: verum