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