theorem Th6: :: MATRIX15:6

for f being FinSequence of NAT
for n being Nat st f is one-to-one & rng f c= Seg n & ( for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ) holds
Sgm (rng f) = f