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

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

hence
a |^ k in gr {(a |^ s)}
by GR_CY_1:5; :: thesis: verum
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;take p9 ; :: thesis: a |^ k = (a |^ s) |^ p9

thus a |^ k = (a |^ s) |^ p9 by A1, GROUP_1:35; :: thesis: verum