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 (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,REAL ; :: 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 A1: ( x in dom (lim f) & f # x is convergent ) ; :: thesis: ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
then x in dom (f . 0 ) by MESFUNC8:def 10;
then ( x in dom (lim_sup f) & x in dom (lim_inf f) ) by MESFUNC8:def 8, MESFUNC8:def 9;
then A2: ( (lim_sup f) . x = lim_sup (R_EAL (f # x)) & (lim_inf f) . x = lim_inf (R_EAL (f # x)) ) by Def8a, Def9a;
R_EAL (f # x) is convergent by A1, RINFSUP2:14;
then ( lim (R_EAL (f # x)) = lim_sup (R_EAL (f # x)) & lim (R_EAL (f # x)) = lim_inf (R_EAL (f # x)) ) by RINFSUP2:41;
hence ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) by A1, A2, Def10a; :: thesis: verum