theorem Th105: :: FINSEQ_3:107

for i, m, n being Nat st n = m + 1 & i in Seg n holds
len (Sgm ((Seg n) \ {i})) = m