for h being Element of (Image g) holds h is p -power

proof

let h be Element of (Image g); :: thesis: h is p -power
h in Image g ;
then consider a being Element of G such that
A1: h = g . a by GROUP_6:45;
consider n being Nat such that
A2: ord a = p |^ n by Def1;
A3: g . (a |^ (p |^ n)) = (g . a) |^ (p |^ n) by GROUP_6:37
.= h |^ (p |^ n) by A1, GROUP_8:4 ;
A4: g . (a |^ (p |^ n)) = g . (1_ G) by A2, GROUP_1:41
.= 1_ H by GROUP_6:31 ;
reconsider h1 = h as Element of H by GROUP_2:42;
h1 |^ (p |^ n) = 1_ H by A3, A4, GROUP_8:4;
then consider r being Nat such that
A5: ( ord h1 = p |^ r & r <= n ) by Th2, GROUP_1:44;
ord h = p |^ r by A5, GROUP_8:5;
hence h is p -power ; :: thesis: verum

end;

hence Image g is p -group by Th17; :: thesis: verum