theorem Th73: :: NUMBER14:73

for m, n being Nat holds card (seq (m,n)) = n