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

assume A4:
for x being object holds f . x < +infty
; :: thesis: f is without+infty assume
f is without+infty
; :: thesis: for x being object holds f . x < +infty

then A3: not +infty in rng f ;

end;then A3: 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 A4; :: thesis: verum

end;then ex x being object st

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

hence contradiction by A4; :: thesis: verum