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