let n, m, i be natural number ; :: thesis: ( n = m + 1 & i in Seg n implies len (Sgm ((Seg n) \ {i})) = m )
assume A1: ( n = m + 1 & i in Seg n ) ; :: thesis: len (Sgm ((Seg n) \ {i})) = m
set X = (Seg n) \ {i};
A2: ( (Seg n) \ {i} c= Seg n & i in {i} ) by TARSKI:def 1, XBOOLE_1:36;
then ( not i in (Seg n) \ {i} & Seg n is finite ) by XBOOLE_0:def 5;
then (card ((Seg n) \ {i})) + 1 = card (((Seg n) \ {i}) \/ {i}) by CARD_2:54
.= card ((Seg n) \/ {i}) by XBOOLE_1:39
.= card (Seg n) by A1, ZFMISC_1:46
.= m + 1 by A1, FINSEQ_1:78 ;
hence len (Sgm ((Seg n) \ {i})) = m by A2, Th44; :: thesis: verum