let n be Element of NAT ; :: thesis: for D being non empty set
for f being FinSequence of D st n in dom f holds
ex k being Element of 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 Element of 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 Element of 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 Element of NAT st
( k in dom (Rev f) & n + k = (len f) + 1 & f /. n = (Rev f) /. k )
then A2: ( 1 <= n & n <= len f ) by FINSEQ_3:27;
take k = ((len f) + 1) -' n; :: thesis: ( k in dom (Rev f) & n + k = (len f) + 1 & f /. n = (Rev f) /. k )
n <= (len f) + 1 by A2, XREAL_1:147;
then A3: k + n = (len f) + 1 by XREAL_1:237;
then A4: (k + n) -' 1 = len f by NAT_D:34;
n + 1 <= (len f) + 1 by A2, XREAL_1:8;
then A5: 1 <= k by NAT_D:55;
k + 1 <= k + n by A2, XREAL_1:8;
then (k + 1) -' 1 <= (k + n) -' 1 by NAT_D:42;
then k <= len f by A4, NAT_D:34;
then k in dom f by A5, FINSEQ_3:27;
hence ( k in dom (Rev f) & n + k = (len f) + 1 & f /. n = (Rev f) /. k ) by A1, A3, FINSEQ_5:60, FINSEQ_5:69; :: thesis: verum