hereby :: thesis: ( ( for x being set holds -infty < f . x ) implies f is without-infty )

assume f is without-infty ; :: thesis: for x being set holds -infty < f . x
then A1: not -infty in rng f by Def3;

hereby :: thesis: verum

let x be set ; :: thesis: -infty < f . b₁

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

suppose x in dom f ; :: thesis: -infty < f . b₁

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

end;

suppose not x in dom f ; :: thesis: -infty < f . b₁

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

end;

end;

end;

end;

assume A2: for x being set holds -infty < f . x ; :: thesis: f is without-infty

now

assume -infty in rng f ; :: thesis: contradiction
then consider x being set such that
A3: ( x in dom f & f . x = -infty ) by FUNCT_1:def 5;
thus contradiction by A2, A3; :: thesis: verum

end;

hence f is without-infty by Def3; :: thesis: verum