let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 1 <= k implies pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1)) )
assume 1 <= k ; :: thesis: 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)) ; :: thesis: verum