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

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

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

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

-infty < f . x

hence for x being set st x in dom f holds

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

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

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

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

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

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

-infty < f . x )

assume
f is ()
; :: thesis: for x being set st x in dom f holds -infty < f . x )

assume A1:
for x being set st x in dom f holds

-infty < f . x ; :: thesis: f is ()

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

now :: thesis: for x being object holds -infty < f . xend;

hence
f is ()
; :: thesis: verum-infty < f . x

hence for x being set st x in dom f holds

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