let i, m, n be Nat; :: thesis: ( n = m + 1 & i in Seg n implies len (Sgm ((Seg n) \ {i})) = m )
assume that
A1: n = m + 1 and
A2: i in Seg n ; :: thesis: len (Sgm ((Seg n) \ {i})) = m
set X = (Seg n) \ {i};
i in {i} by TARSKI:def 1;
then not i in (Seg n) \ {i} by XBOOLE_0:def 5;
then (card ((Seg n) \ {i})) + 1 = card (((Seg n) \ {i}) \/ {i}) by CARD_2:41
.= card ((Seg n) \/ {i}) by XBOOLE_1:39
.= card (Seg n) by A2, ZFMISC_1:40
.= m + 1 by A1, FINSEQ_1:57 ;
hence len (Sgm ((Seg n) \ {i})) = m by Th37, XBOOLE_1:36; :: thesis: verum