theorem Th6: :: MATRIX15:6

for f being natural-valued FinSequence st rng f is included_in_Seg & f is increasing holds
Sgm (rng f) = f