theorem Th5: :: CALCUL_2:5

for a, b being Nat holds (seq (a,b)) \/ {((a + b) + 1)} = seq (a,(b + 1))