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