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

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