theorem :: STIRL2_1:30

for n being Nat holds
( n block 0 = 1 iff n = 0 )