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

assume f is without+infty ; :: thesis: for x being set holds f . x < +infty
then A4: not +infty in rng f by Def4;

hereby :: thesis: verum

let x be set ; :: 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 A4, FUNCT_1:def 5;
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 4; :: thesis: verum

end;

end;

end;

end;

assume A5: for x being set holds f . x < +infty ; :: thesis: f is without+infty

now

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

end;

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