let X be BCI-algebra; :: thesis: for n being Nat holds ((0. X),(0. X)) to_power n = 0. X
let n be Nat; :: thesis: ((0. X),(0. X)) to_power n = 0. X
defpred S₁[ set ] means for m being Nat st m = $1 & m <= n holds
((0. X),(0. X)) to_power m = 0. X;
A1: for k being Nat st S₁[k] holds
S₁[k + 1] by Th5;
A2: S₁[ 0 ] by Th1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A1);
hence ((0. X),(0. X)) to_power n = 0. X ; :: thesis: verum