dom f <> {} ;
hence not Rev f is empty by FINSEQ_5:57, RELAT_1:38; :: thesis: verum