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