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

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