let n be Element of NAT ; :: thesis: for D being non empty set
for f being FinSequence of D st n in dom (Rev f) holds
ex k being Element of NAT st
( k in dom f & n + k = (len f) + 1 & (Rev f) /. n = f /. k )
let D be non empty set ; :: thesis: for f being FinSequence of D st n in dom (Rev f) holds
ex k being Element of NAT st
( k in dom f & n + k = (len f) + 1 & (Rev f) /. n = f /. k )
let f be FinSequence of D; :: thesis: ( n in dom (Rev f) implies ex k being Element of NAT st
( k in dom f & n + k = (len f) + 1 & (Rev f) /. n = f /. k ) )
assume n in dom (Rev f) ; :: thesis: ex k being Element of NAT st
( k in dom f & n + k = (len f) + 1 & (Rev f) /. n = f /. k )
then n in dom f by FINSEQ_5:60;
then consider k being Element of NAT such that
A1: k in dom (Rev f) and
A2: n + k = (len f) + 1 and
f /. n = (Rev f) /. k by Th5;
A3: ( len f = len (Rev f) & dom f = dom (Rev f) ) by FINSEQ_5:60, FINSEQ_5:def 3;
then (Rev f) /. n = f /. k by A1, A2, FINSEQ_5:69;
hence ex k being Element of NAT st
( k in dom f & n + k = (len f) + 1 & (Rev f) /. n = f /. k ) by A1, A2, A3; :: thesis: verum