theorem Th90: :: FINSEQ_3:92

for A being set
for k being Nat st A c= Seg k holds
Sgm A is one-to-one by Lm1;