let n be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st n in dom f holds
ex k being Nat st
( k in dom (Rev f) & n + k = (len f) + 1 & f /. n = (Rev f) /. k )
let D be non empty set ; :: thesis: for f being FinSequence of D st n in dom f holds
ex k being Nat st
( k in dom (Rev f) & n + k = (len f) + 1 & f /. n = (Rev f) /. k )
let f be FinSequence of D; :: thesis: ( n in dom f implies ex k being Nat st
( k in dom (Rev f) & n + k = (len f) + 1 & f /. n = (Rev f) /. k ) )
assume A1: n in dom f ; :: thesis: ex k being Nat st
( k in dom (Rev f) & n + k = (len f) + 1 & f /. n = (Rev f) /. k )
take k = ((len f) + 1) -' n; :: thesis: ( k in dom (Rev f) & n + k = (len f) + 1 & f /. n = (Rev f) /. k )
1 <= n by A1, FINSEQ_3:25;
then k + 1 <= k + n by XREAL_1:6;
then A2: (k + 1) -' 1 <= (k + n) -' 1 by NAT_D:42;
A3: n <= len f by A1, FINSEQ_3:25;
then n + 1 <= (len f) + 1 by XREAL_1:6;
then A4: 1 <= k by NAT_D:55;
n <= (len f) + 1 by A3, XREAL_1:145;
then A5: k + n = (len f) + 1 by XREAL_1:235;
then (k + n) -' 1 = len f by NAT_D:34;
then k <= len f by A2, NAT_D:34;
then k in dom f by A4, FINSEQ_3:25;
hence ( k in dom (Rev f) & n + k = (len f) + 1 & f /. n = (Rev f) /. k ) by A1, A5, FINSEQ_5:57, FINSEQ_5:66; :: thesis: verum