let i, n be Nat; :: thesis: ( i in Seg n implies (n - i) + 1 in Seg n )
assume A1: i in Seg n ; :: thesis: (n - i) + 1 in Seg n
then ( 1 <= i & i <= n ) by FINSEQ_1:3;
then reconsider ni = n - i as Element of NAT by INT_1:18;
reconsider j = ni + 1 as Element of NAT ;
A2: 0 + 1 <= j by XREAL_1:8;
ni <= n by XREAL_1:45;
then A3: j <= n + 1 by XREAL_1:8;

now

assume j = n + 1 ; :: thesis: contradiction
then - 0 = - i ;
hence contradiction by A1, FINSEQ_1:3; :: thesis: verum

end;

then j < n + 1 by A3, XXREAL_0:1;
then j <= n by NAT_1:13;
hence (n - i) + 1 in Seg n by A2; :: thesis: verum