let G be Group; :: thesis: for a being Element of G
for k, s being Element of NAT st s divides k holds
a |^ k in gr {(a |^ s)}
let a be Element of G; :: thesis: for k, s being Element of NAT st s divides k holds
a |^ k in gr {(a |^ s)}
let k, s be Element of NAT ; :: thesis: ( s divides k implies a |^ k in gr {(a |^ s)} )
assume s divides k ; :: thesis: a |^ k in gr {(a |^ s)}
then consider p being Nat such that
A1: k = s * p by NAT_D:def 3;
ex i being Integer st a |^ k = (a |^ s) |^ i

proof

reconsider p9 = p as Integer ;
take p9 ; :: thesis: a |^ k = (a |^ s) |^ p9
thus a |^ k = (a |^ s) |^ p9 by A1, GROUP_1:35; :: thesis: verum

end;

hence a |^ k in gr {(a |^ s)} by GR_CY_1:5; :: thesis: verum