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

now :: thesis: for i being Nat st i in dom (Rev f) holds
(Rev f) . i in D

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 ((len f) - i) + 1 in Seg (len f) by Th2;
then f . (((len f) - i) + 1) in D by A1, FINSEQ_2:11;
hence (Rev f) . i in D by A1, A2, Th58; :: thesis: verum

end;

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