set R = Inv f;
assume not Inv f is non-empty ; :: thesis: contradiction
then 0 in rng (Inv f) ;
then consider x being object such that
A1: x in dom (Inv f) and
A2: (Inv f) . x = 0 by FUNCT_1:def 3;
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 by A1, ORDINAL1:def 16;
not a " is zero ;
hence contradiction by A2, VALUED_1:10; :: thesis: verum