theorem Th77: :: NUMBER19:77

for n, m, k being Nat holds (seq (n,m)) \/ (seq ((n + m),k)) = seq (n,(m + k))