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

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