theorem Th2: :: CALCUL_2:2

for a being Nat holds seq (a,0) = {}