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