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 () )

let f be PartFunc of X,ExtREAL; :: thesis: ( ( for x being set st x in dom f holds

f . x < +infty ) iff f is () )

f . x < +infty

hence for x being set st x in dom f holds

f . x < +infty ; :: thesis: verum

( ( for x being set st x in dom f holds

f . x < +infty ) iff f is () )

let f be PartFunc of X,ExtREAL; :: thesis: ( ( for x being set st x in dom f holds

f . x < +infty ) iff f is () )

hereby :: thesis: ( f is () implies for x being set st x in dom f holds

f . x < +infty )

assume
f is ()
; :: thesis: 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 ()

end;f . x < +infty ; :: thesis: f is ()

now :: thesis: for x being object holds f . x < +infty end;

hence
f is ()
; :: thesis: verumf . x < +infty

hence for x being set st x in dom f holds

f . x < +infty ; :: thesis: verum