theorem Th11: :: MESFUNC8:11

for X being non empty set
for f being Functional_Sequence of X,ExtREAL holds
( ( for x being Element of X st x in dom (lim_inf f) holds
( (lim_inf f) . x = sup (inferior_realsequence (f # x)) & (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) ) & lim_inf f = sup (inferior_realsequence f) )