theorem Th1: :: FINSEQ_6:1

for X being set
for i being Nat st X c= Seg i & 1 in X holds
(Sgm X) . 1 = 1