let i, n be Nat; :: thesis: ( i > 1 & i in Seg n implies i -' 1 in Seg n )
assume that
A1: i > 1 and
A2: i in Seg n ; :: thesis: i -' 1 in Seg n
i - 1 > 1 - 1 by A1, XREAL_1:9;
then i -' 1 > 0 by A1, XREAL_1:233;
then A3: i -' 1 >= 0 + 1 by NAT_1:13;
i <= n by A2, FINSEQ_1:1;
then i -' 1 <= n by NAT_D:44;
hence i -' 1 in Seg n by A3, FINSEQ_1:1; :: thesis: verum