let i, n be Nat; :: thesis: ( i in Seg n implies (n -' i) + 1 in Seg n )
A1: 1 <= (n -' i) + 1 by NAT_1:11;
assume A2: i in Seg n ; :: thesis: (n -' i) + 1 in Seg n
then 1 <= i by FINSEQ_1:3;
then n - i <= n - 1 by XREAL_1:15;
then A3: (n - i) + 1 <= n by XREAL_1:21;
i <= n by A2, FINSEQ_1:3;
then (n -' i) + 1 <= n by A3, XREAL_1:235;
hence (n -' i) + 1 in Seg n by A1, FINSEQ_1:3; :: thesis: verum