let F1 be FinSequence; :: thesis: for y being Element of NAT st y in dom F1 holds
( ((len F1) - y) + 1 is Element of NAT & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 )
let y be Element of NAT ; :: thesis: ( y in dom F1 implies ( ((len F1) - y) + 1 is Element of NAT & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 ) )
assume A1: y in dom F1 ; :: thesis: ( ((len F1) - y) + 1 is Element of NAT & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 )
now :: thesis: not ((len F1) - y) + 1 < 0
assume ((len F1) - y) + 1 < 0 ; :: thesis: contradiction
then 1 < 0 - ((len F1) - y) by XREAL_1:20;
then 1 < y - (len F1) ;
then A2: (len F1) + 1 < y by XREAL_1:20;
y <= len F1 by A1, FINSEQ_3:25;
hence contradiction by A2, NAT_1:12; :: thesis: verum
end;
then reconsider n = ((len F1) - y) + 1 as Element of NAT by INT_1:3;
y >= 1 by A1, FINSEQ_3:25;
then (n - 1) - y <= ((len F1) - y) - 1 by XREAL_1:13;
then A3: n - (y + 1) <= (len F1) - (y + 1) ;
y + 0 <= len F1 by A1, FINSEQ_3:25;
then ( 0 + 1 = 1 & 0 <= (len F1) - y ) by XREAL_1:19;
hence ( ((len F1) - y) + 1 is Element of NAT & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 ) by A3, XREAL_1:6, XREAL_1:9; :: thesis: verum