let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; :: thesis: for x being Element of L
for n, m being Element of NAT holds pow x,(n * m) = pow (pow x,n),m
let x be Element of L; :: thesis: for n, m being Element of NAT holds pow x,(n * m) = pow (pow x,n),m
let n, m be Element of NAT ; :: thesis: pow x,(n * m) = pow (pow x,n),m
pow x,(n * m) = x |^ (n * m) by Def3
.= (x |^ n) |^ m by BINOM:12
.= pow (x |^ n),m by Def3
.= pow (pow x,n),m by Def3 ;
hence pow x,(n * m) = pow (pow x,n),m ; :: thesis: verum