theorem Th7: :: BCIALG_6:7

for X being BCI-algebra
for n being Nat holds (0. X) |^ n = 0. X