let m, n be Element of 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:54, FINSEQ_3:11;
then A3: card ((Seg n) \/ {(n + m)}) = n + 1 by FINSEQ_1:78;
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:3;
then A4: {(n + m)} c= Seg (n + m) by ZFMISC_1:37;
Seg n c= Seg (n + m) by FINSEQ_3:19;
hence len (Sgm ((Seg n) \/ {(n + m)})) = n + 1 by A3, A4, FINSEQ_3:44, XBOOLE_1:8; :: thesis: verum