let i, n be Nat; :: thesis: ( i in Seg n implies i + 1 in Seg (n + 1) )
assume i in Seg n ; :: thesis: i + 1 in Seg (n + 1)
then ( 1 <= i & i <= n ) by FINSEQ_1:3;
then ( 1 + 1 <= i + 1 & i + 1 <= n + 1 ) by XREAL_1:8;
then ( 1 <= i + 1 & i + 1 <= n + 1 ) by XXREAL_0:2;
hence i + 1 in Seg (n + 1) by FINSEQ_1:3; :: thesis: verum