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 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 )

R_EAL (f # x) is convergent by A2, RINFSUP2:14;

then A3: ( 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;

A4: x in dom (f . 0) by A1, MESFUNC8:def 9;

then x in dom (lim_inf f) by MESFUNC8:def 7;

then A5: (lim_inf f) . x = lim_inf (R_EAL (f # x)) by Th12;

x in dom (lim_sup f) by A4, MESFUNC8:def 8;

then (lim_sup f) . x = lim_sup (R_EAL (f # x)) by Th13;

hence ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) by A1, A5, A3, Th14; :: thesis: verum

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 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 )

R_EAL (f # x) is convergent by A2, RINFSUP2:14;

then A3: ( 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;

A4: x in dom (f . 0) by A1, MESFUNC8:def 9;

then x in dom (lim_inf f) by MESFUNC8:def 7;

then A5: (lim_inf f) . x = lim_inf (R_EAL (f # x)) by Th12;

x in dom (lim_sup f) by A4, MESFUNC8:def 8;

then (lim_sup f) . x = lim_sup (R_EAL (f # x)) by Th13;

hence ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) by A1, A5, A3, Th14; :: thesis: verum