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 i <= n by FINSEQ_1:1;
then reconsider ni = n - i as Element of NAT by INT_1:5;
reconsider j = ni + 1 as Element of NAT ;

A2: now :: thesis: not j = n + 1

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

end;

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