per cases ( i in dom f or not i in dom f ) ;

suppose i in dom f ; :: thesis: not f . i is positive

then f . i in rng f by FUNCT_1:3;
hence not f . i is positive by PARTFUN3:def 3; :: thesis: verum

end;

suppose not i in dom f ; :: thesis: not f . i is positive

hence not f . i is positive by FUNCT_1:def 2; :: thesis: verum

end;

end;