for n being Nat holds n block n = 1