hereby :: thesis:

assume f is without-infty ; :: thesis:
then A1: not -infty in rng f ;

hereby :: thesis:

let x be object ; :: thesis:

per cases ;

suppose x in dom f ; :: thesis:

then f . x <> -infty by A1, FUNCT_1:def 3;
hence -infty < f . x by XXREAL_0:6; :: thesis:

end;

suppose not x in dom f ; :: thesis:

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

end;

end;

end;

end;

assume A2: for x being object holds -infty < f . x ; :: thesis:

now :: thesis:

assume -infty in rng f ; :: thesis:
then ex x being object st
( x in dom f & f . x = -infty ) by FUNCT_1:def 3;
hence contradiction by A2; :: thesis:

end;

hence f is without-infty ; :: thesis: