for k being Nat holds
( 0 block k = 1 iff k = 0 ) by Th26, Th27;