let f be V183() Function of [:NAT,NAT:],ExtREAL; :: thesis: ( sup (rng f) in REAL or sup (rng f) = +infty )
A1: not -infty in rng f by MESFUNC5:def 3;
dom f = [:NAT,NAT:] by FUNCT_2:def 1;
then [1,1] in dom f by ZFMISC_1:87;
then f . (1,1) in rng f by FUNCT_1:3;
then -infty is not UpperBound of rng f by A1, XXREAL_0:6, XXREAL_2:def 1;
then sup (rng f) <> -infty by XXREAL_2:def 3;
hence ( sup (rng f) in REAL or sup (rng f) = +infty ) by XXREAL_0:14; :: thesis: verum