theorem Th106: :: FINSEQ_3:108

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