theorem Th2: :: NUMBER11:2

for n, b being Nat holds value (<%n%>,b) = n