let X be BCI-algebra; :: thesis: for x being Element of X
for n being Nat holds x |^ (n + 1) = x \ ((x |^ n) `)
let x be Element of X; :: thesis: for n being Nat holds x |^ (n + 1) = x \ ((x |^ n) `)
let n be Nat; :: thesis: x |^ (n + 1) = x \ ((x |^ n) `)
reconsider n = n as Element of NAT by ORDINAL1:def 12;
x |^ (n + 1) = x \ ((x |^ n) `) by Def1;
hence x |^ (n + 1) = x \ ((x |^ n) `) ; :: thesis: verum