theorem Th27: :: STIRL2_1:27

for k being Nat st k <> 0 holds
0 block k = 0