let X be non empty set ; :: thesis: for Y being non empty Subset of ExtREAL
for F being Function of X,Y
for x being Element of X st Y c= REAL holds
( -infty < F . x & F . x < +infty )
let Y be non empty Subset of ExtREAL; :: thesis: for F being Function of X,Y
for x being Element of X st Y c= REAL holds
( -infty < F . x & F . x < +infty )
let F be Function of X,Y; :: thesis: for x being Element of X st Y c= REAL holds
( -infty < F . x & F . x < +infty )
let x be Element of X; :: thesis: ( Y c= REAL implies ( -infty < F . x & F . x < +infty ) )
A1: -infty <= F . x by XXREAL_0:5;
assume Y c= REAL ; :: thesis: ( -infty < F . x & F . x < +infty )
hence ( -infty < F . x & F . x < +infty ) by A1, XXREAL_0:1, XXREAL_0:4; :: thesis: verum