let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ; for x being Element of L
for i, k being Element of NAT st 1 <= k holds
pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1))
let x be Element of L; for i, k being Element of NAT st 1 <= k holds
pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1))
let i, k be Element of NAT ; ( 1 <= k implies pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1)) )
assume
1 <= k
; pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1))
then
0 < k
;
then reconsider m = k - 1 as Element of NAT by NAT_1:20;
pow (x,(i * (k - 1))) =
x |^ (i * m)
by Def2
.=
(x |^ i) |^ m
by BINOM:11
.=
pow ((x |^ i),m)
by Def2
;
hence
pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1))
; verum