let X be BCI-algebra; :: thesis: for x, y being Element of X
for n being Nat holds ((0. X),(x \ y)) to_power n = (((0. X),x) to_power n) \ (((0. X),y) to_power n)
let x, y be Element of X; :: thesis: for n being Nat holds ((0. X),(x \ y)) to_power n = (((0. X),x) to_power n) \ (((0. X),y) to_power n)
let n be Nat; :: thesis: ((0. X),(x \ y)) to_power n = (((0. X),x) to_power n) \ (((0. X),y) to_power n)
defpred S₁[ set ] means for m being Nat st m = $1 & m <= n holds
((0. X),(x \ y)) to_power m = (((0. X),x) to_power m) \ (((0. X),y) to_power m);
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: for m being Nat st m = k & m <= n holds
((0. X),(x \ y)) to_power m = (((0. X),x) to_power m) \ (((0. X),y) to_power m) ; :: thesis: S₁[k + 1]
let m be Nat; :: thesis: ( m = k + 1 & m <= n implies ((0. X),(x \ y)) to_power m = (((0. X),x) to_power m) \ (((0. X),y) to_power m) )
assume that
A3: m = k + 1 and
A4: m <= n ; :: thesis: ((0. X),(x \ y)) to_power m = (((0. X),x) to_power m) \ (((0. X),y) to_power m)
k <= n by A3, A4, NAT_1:13;
then ((0. X),(x \ y)) to_power k = (((0. X),x) to_power k) \ (((0. X),y) to_power k) by A2;
then ((0. X),(x \ y)) to_power (k + 1) = ((((0. X),x) to_power k) \ (((0. X),y) to_power k)) \ (x \ y) by Th4
.= ((((0. X),x) to_power k) \ (x \ y)) \ (((0. X),y) to_power k) by BCIALG_1:7
.= ((((x \ y) `),x) to_power k) \ (((0. X),y) to_power k) by Th7
.= ((((x `) \ (y `)),x) to_power k) \ (((0. X),y) to_power k) by BCIALG_1:9
.= ((((x `),x) to_power k) \ (y `)) \ (((0. X),y) to_power k) by Th7
.= ((((x `),x) to_power k) \ (((0. X),y) to_power k)) \ (y `) by BCIALG_1:7
.= (((((0. X),x) to_power k) \ x) \ (((0. X),y) to_power k)) \ (y `) by Th7 ;
then ((0. X),(x \ y)) to_power (k + 1) = ((((0. X),x) to_power (k + 1)) \ (((0. X),y) to_power k)) \ (y `) by Th4
.= ((((0. X),x) to_power (k + 1)) \ (y `)) \ (((0. X),y) to_power k) by BCIALG_1:7
.= ((((y `) `),x) to_power (k + 1)) \ (((0. X),y) to_power k) by Th7
.= ((((y `) `) \ (((0. X),y) to_power k)),x) to_power (k + 1) by Th7
.= ((((((0. X),y) to_power k) `) \ (y `)),x) to_power (k + 1) by BCIALG_1:7
.= ((((((0. X),y) to_power k) \ y) `),x) to_power (k + 1) by BCIALG_1:9
.= (((((0. X),y) to_power (k + 1)) `),x) to_power (k + 1) by Th4 ;
hence ((0. X),(x \ y)) to_power m = (((0. X),x) to_power m) \ (((0. X),y) to_power m) by A3, Th7; :: thesis: verum

end;

(0. X) ` = 0. X by BCIALG_1:def 5;
then ((0. X),(x \ y)) to_power 0 = (0. X) ` by Th1;
then ((0. X),(x \ y)) to_power 0 = (((0. X),x) to_power 0) \ (0. X) by Th1;
then A5: S₁[ 0 ] by Th1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A1);
hence ((0. X),(x \ y)) to_power n = (((0. X),x) to_power n) \ (((0. X),y) to_power n) ; :: thesis: verum