let f be FinSequence; :: thesis: f, Rev f are_fiberwise_equipotent
A1: f = (Rev f) * (Rev (idseq (len f))) by REV;
Rev (idseq (len f)) is Permutation of (dom (Rev f)) by RFP;
hence f, Rev f are_fiberwise_equipotent by A1, RFINSEQ:4; :: thesis: verum