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