theorem Th6: :: CALCUL_2:6

for m, n being Element of NAT holds seq (m,n),n are_equipotent