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 (f . 0 ) holds
( f # x is convergent iff (lim_sup 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 (f . 0 ) holds
( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x )
let x be Element of X; :: thesis: ( x in dom (f . 0 ) implies ( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x ) )
assume A1: x in dom (f . 0 ) ; :: thesis: ( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x )
then x in dom (lim_inf f) by Def8;
then A2: (lim_inf f) . x = lim_inf (f # x) by Def8;
x in dom (lim_sup f) by A1, Def9;
then (lim_sup f) . x = lim_sup (f # x) by Def9;
hence ( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x ) by A2, RINFSUP2:40; :: thesis: verum