let X be non empty set ; :: thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (f . 0 ) & f # x is convergent holds
(superior_realsequence f) # x is bounded_below
let f be Functional_Sequence of X,REAL ; :: thesis: for x being Element of X st x in dom (f . 0 ) & f # x is convergent holds
(superior_realsequence f) # x is bounded_below
let x be Element of X; :: thesis: ( x in dom (f . 0 ) & f # x is convergent implies (superior_realsequence f) # x is bounded_below )
assume A1: x in dom (f . 0 ) ; :: thesis: ( not f # x is convergent or (superior_realsequence f) # x is bounded_below )
assume f # x is convergent ; :: thesis: (superior_realsequence f) # x is bounded_below
then A2: f # x is bounded by RINFSUP1:90;
then A3: superior_realsequence (f # x) is bounded by RINFSUP1:58;
superior_realsequence (R_EAL (f # x)) = superior_realsequence (f # x) by A2, RINFSUP2:9;
then (superior_realsequence f) # x = superior_realsequence (f # x) by A1, Th10;
hence (superior_realsequence f) # x is bounded_below by A3, RINFSUP2:13; :: thesis: verum