theorem Th29: :: NAT_5:29

for k being Nat holds sigma (k,1) = 1