let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ; 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; for n, m being Element of NAT holds pow (x,(n * m)) = pow ((pow (x,n)),m)
let n, m be Element of NAT ; 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)
; verum