let m, n be Nat; :: thesis: ( 0 < m implies len (Sgm ((Seg n) \/ {(n + m)})) = n + 1 )
A1: m <= n + m by NAT_1:11;
assume A2: 0 < m ; :: thesis: len (Sgm ((Seg n) \/ {(n + m)})) = n + 1
then card ((Seg n) \/ {(n + m)}) = (card (Seg n)) + 1 by CARD_2:41, FINSEQ_3:10;
then A3: card ((Seg n) \/ {(n + m)}) = n + 1 by FINSEQ_1:57;
0 + 1 <= m by A2, NAT_1:13;
then 1 <= m + n by A1, XXREAL_0:2;
then n + m in Seg (n + m) by FINSEQ_1:1;
then A4: {(n + m)} c= Seg (n + m) by ZFMISC_1:31;
Seg n c= Seg (n + m) by FINSEQ_3:18;
hence len (Sgm ((Seg n) \/ {(n + m)})) = n + 1 by A3, A4, FINSEQ_3:39, XBOOLE_1:8; :: thesis: verum