per cases ( i in dom f or not i in dom f ) ;
suppose i in dom f ; :: thesis: not f . i is negative
then f . i in rng f by FUNCT_1:def 3;
hence not f . i is negative by PARTFUN3:def 4; :: thesis: verum
end;
suppose not i in dom f ; :: thesis: not f . i is negative
hence not f . i is negative by FUNCT_1:def 2; :: thesis: verum
end;
end;