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

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