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