theorem Th6: :: CALCUL_2:6

for a, b being Nat holds seq (a,b),b are_equipotent