theorem Th6: :: BCIALG_2:6

for X being BCI-algebra
for n being Nat holds ((0. X),(0. X)) to_power n = 0. X