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

proof

let h be Element of (Image g); :: thesis: h is p -element
h in Image g by STRUCT_0:def 5;
then consider a being Element of G such that
A2: h = g . a by GROUP_6:54;
consider n being natural number such that
A3: ord a = p |^ n by def1;
A4: g . (a |^ (p |^ n)) = (g . a) |^ (p |^ n) by GROUP_6:46
.= h |^ (p |^ n) by A2, GROUP_8:4 ;
A5: g . (a |^ (p |^ n)) = g . (1_ G) by A3, GROUP_1:82
.= 1_ H by GROUP_6:40 ;
reconsider h1 = h as Element of H by GROUP_2:51;
h1 |^ (p |^ n) = 1_ H by A4, A5, GROUP_8:4;
then consider r being natural number such that
A7: ( ord h1 = p |^ r & r <= n ) by GROUP_1:86, Th2;
ord h = p |^ r by A7, GROUP_8:5;
hence h is p -element by def1; :: thesis: verum

end;

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