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 {(n + m)} c= Seg (n + m) by ZFMISC_1:31;
then {(n + m)} is included_in_Seg by FINSEQ_1:def 13;
hence len (Sgm ((Seg n) \/ {(n + m)})) = n + 1 by A3, FINSEQ_3:39; :: thesis: verum