let L be non empty almost_left_invertible associative commutative well-unital distributive 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 Def3
.= (x |^ i) |^ m by BINOM:12
.= pow (x |^ i),m by Def3 ;
hence pow x,(i * (k - 1)) = pow (x |^ i),(k - 1) ; :: thesis: verum