let n be Nat; :: thesis: for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr
for a being Element of K holds a |^ (n + 1) = (a |^ n) * a
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; :: thesis: for a being Element of K holds a |^ (n + 1) = (a |^ n) * a
let a be Element of K; :: thesis: a |^ (n + 1) = (a |^ n) * a
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
thus a |^ (n + 1) = ((power K) . (a,n1)) * a by GROUP_1:def 7
.= (a |^ n) * a ; :: thesis: verum