let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL holds
( ( for x being set st x in dom f holds
f . x < +infty ) iff f is without+infty )
let f be PartFunc of X,ExtREAL; :: thesis: ( ( for x being set st x in dom f holds
f . x < +infty ) iff f is without+infty )

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

assume A1: for x being set st x in dom f holds
f . x < +infty ; :: thesis: f is without+infty

now

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

hence f . x < +infty by A1; :: 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;

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

end;

assume f is without+infty ; :: thesis: for x being set st x in dom f holds
f . x < +infty
hence for x being set st x in dom f holds
f . x < +infty by Def6; :: thesis: verum