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 13;
x |^ (n + 1) = x \ ((x |^ n) ` ) by Def1;
hence x |^ (n + 1) = x \ ((x |^ n) ` ) ; :: thesis: verum