theorem Th7: :: CALCUL_2:7

for m, n being Element of NAT holds seq (m,n) c= Seg (m + n)