let K be non empty unital associative multMagma ; :: thesis: for a being Element of K
for n being Nat holds a |^ (n + 1) = (a |^ n) * a
let a be Element of K; :: thesis: for n being Nat holds a |^ (n + 1) = (a |^ n) * a
let n be Nat; :: thesis: a |^ (n + 1) = (a |^ n) * a
a |^ (n + 1) = (a |^ n) * (a |^ 1) by BINOM:10
.= (a |^ n) * a by BINOM:8 ;
hence a |^ (n + 1) = (a |^ n) * a ; :: thesis: verum