set R = Inv f;
assume not Inv f is non-empty ; :: thesis: contradiction
then 0 in rng (Inv f) by RELAT_1:def 9;
then consider x being set such that
A1: x in dom (Inv f) and
A2: (Inv f) . x = 0 by FUNCT_1:def 5;
dom (Inv f) = X by FUNCT_2:def 1
.= dom f by FUNCT_2:def 1 ;
then reconsider a = f . x as non zero real number by A1;
not a " is empty ;
hence contradiction by A2, VALUED_1:10; :: thesis: verum