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