let f be FinSequence; :: thesis: for P being Permutation of (dom f) holds P is Permutation of (dom (Rev f))
let P be Permutation of (dom f); :: thesis: P is Permutation of (dom (Rev f))
len f = len (Rev f) by FINSEQ_5:def 3;
then dom f = dom (Rev f) by FINSEQ_3:29;
hence P is Permutation of (dom (Rev f)) ; :: thesis: verum