theorem :: FINSEQ_3:152

for X being set
for k being Element of NAT st X c= Seg k holds
for m, n being Element of NAT st m in dom (Sgm X) & n = (Sgm X) . m holds
m <= n