rng {} = {} ;
hence {} is onto by FUNCT_2:def 3; :: thesis: verum