hereby :: thesis: ( ( for x being object holds f . x < +infty ) implies 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 ;

hereby :: thesis: verum

let x be object ; :: thesis: f . b₁ < +infty

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

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

then f . x <> +infty by A3, FUNCT_1:def 3;
hence f . x < +infty by XXREAL_0:4; :: thesis: verum

end;

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

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

end;

end;

end;

end;

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

now :: thesis: not +infty in rng f

assume +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;

hence f is without+infty ; :: thesis: verum