let n be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st n in dom (Rev f) holds
ex k being 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 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 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 Nat st
( k in dom f & n + k = (len f) + 1 & (Rev f) /. n = f /. k )
then n in dom f by FINSEQ_5:57;
then consider k being Nat such that
A1: ( k in dom (Rev f) & n + k = (len f) + 1 ) and
f /. n = (Rev f) /. k by Th3;
A2: dom f = dom (Rev f) by FINSEQ_5:57;
then (Rev f) /. n = f /. k by A1, FINSEQ_5:66;
hence ex k being Nat st
( k in dom f & n + k = (len f) + 1 & (Rev f) /. n = f /. k ) by A1, A2; :: thesis: verum