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

hereby :: thesis: ( f is () implies 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 ()

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

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

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

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

hence -infty < f . x by A1; :: thesis: verum

end;

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

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

end;

end;

end;

hence f is () ; :: thesis: verum

end;

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