let X be BCI-algebra; for x, y being Element of X holds (x,y) to_power 2 = (x \ y) \ y
let x, y be Element of X; (x,y) to_power 2 = (x \ y) \ y
consider f being sequence of the carrier of X such that
A1:
( (x,y) to_power 2 = f . 2 & f . 0 = x )
and
A2:
for j being Nat st j < 2 holds
f . (j + 1) = (f . j) \ y
by Def1;
1 < 1 + 1
by NAT_1:13;
then
f . (1 + 1) = (f . (0 + 1)) \ y
by A2;
hence
(x,y) to_power 2 = (x \ y) \ y
by A1, A2, NAT_1:3; verum