let X be non empty set ; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:

hereby :: thesis:

assume A1: for x being set st x in dom f holds
-infty < f . x ; :: thesis:

now :: thesis:

let x be object ; :: thesis:

per cases ;

suppose x in dom f ; :: thesis:

hence -infty < f . x by A1; :: thesis:

end;

suppose not x in dom f ; :: thesis:

hence -infty < f . x by FUNCT_1:def 2; :: thesis:

end;

end;

end;

hence f is () ; :: thesis:

end;

assume f is () ; :: thesis:
hence for x being set st x in dom f holds
-infty < f . x ; :: thesis: