theorem Th1: :: FINSEQ_6:1

for X being included_in_Seg set st 1 in X holds
(Sgm X) . 1 = 1