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 ;
then superior_realsequence (R_EAL (f # x)) = superior_realsequence (f # x) by RINFSUP2:9;
then A3: (superior_realsequence f) # x = superior_realsequence (f # x) by A1, Th11;
superior_realsequence (f # x) is bounded by A2, RINFSUP1:56;
hence (superior_realsequence f) # x is bounded_below by A3, RINFSUP2:13; :: thesis: verum