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

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

then A1: not -infty in rng f ;

end;then A1: not -infty in rng f ;

now :: thesis: not -infty in rng f

hence
f is without-infty
; :: thesis: verumassume
-infty in rng f
; :: thesis: contradiction

then ex x being object st

( x in dom f & f . x = -infty ) by FUNCT_1:def 3;

hence contradiction by A2; :: thesis: verum

end;then ex x being object st

( x in dom f & f . x = -infty ) by FUNCT_1:def 3;

hence contradiction by A2; :: thesis: verum