set n = len f;
A1: dom f = Seg (len f) by FINSEQ_1:def 3;

now

let i be Nat; :: thesis: ( i in dom (Rev f) implies (Rev f) . i in D )
set j = ((len f) - i) + 1;
assume i in dom (Rev f) ; :: thesis: (Rev f) . i in D
then i in Seg (len (Rev f)) by FINSEQ_1:def 3;
then A2: i in Seg (len f) by Def3;
then i <= len f by A1, FINSEQ_3:27;
then ( ((len f) - i) + 1 in Seg (len f) & ((len f) - i) + 1 is Element of NAT ) by A2, Th1, Th2;
then f . (((len f) - i) + 1) in D by A1, FINSEQ_2:13;
hence (Rev f) . i in D by A1, A2, Th61; :: thesis: verum

end;

hence Rev f is FinSequence of D by FINSEQ_2:14; :: thesis: verum