let X be non empty set ; :: thesis: for f being Functional_Sequence of X,ExtREAL
for x being Element of X st x in dom (lim f) & f # x is convergent holds
( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
let f be Functional_Sequence of X,ExtREAL; :: thesis: for x being Element of X st x in dom (lim f) & f # x is convergent holds
( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
let x be Element of X; :: thesis: ( x in dom (lim f) & f # x is convergent implies ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) )
assume that
A1: x in dom (lim f) and
A2: f # x is convergent ; :: thesis: ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
A3: lim (f # x) = lim_inf (f # x) by A2, RINFSUP2:41;
A4: x in dom (f . 0) by A1, Def10;
then x in dom (lim_sup f) by Def9;
then A5: (lim_sup f) . x = lim_sup (f # x) by Def9;
x in dom (lim_inf f) by A4, Def8;
then A6: (lim_inf f) . x = lim_inf (f # x) by Def8;
lim (f # x) = lim_sup (f # x) by A2, RINFSUP2:41;
hence ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) by A1, A5, A6, A3, Def10; :: thesis: verum