len (Rev f) = len f by FINSEQ_5:def 3;
then (Rev f) null f is len f -element ;
hence Rev f is len f -element ; :: thesis: verum