let X be non empty set ; :: thesis: 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) )
let f be Functional_Sequence of X,ExtREAL; :: thesis: ( ( 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) )
dom (sup (inferior_realsequence f)) = dom ((inferior_realsequence f) . 0) by Def4;
then dom (sup (inferior_realsequence f)) = dom (f . 0) by Def5;
then A1: dom (sup (inferior_realsequence f)) = dom (lim_inf f) by Def7;

A2: now :: thesis: 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 )

let x be Element of X; :: thesis: ( x in dom (lim_inf f) implies ( (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 ) )
assume A3: x in dom (lim_inf f) ; :: thesis: ( (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 )
then A4: (lim_inf f) . x = lim_inf (f # x) by Def7;
hence (lim_inf f) . x = sup (inferior_realsequence (f # x)) ; :: thesis: ( (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x )
dom (lim_inf f) = dom (f . 0) by Def7;
hence (lim_inf f) . x = sup ((inferior_realsequence f) # x) by A3, A4, Th7; :: thesis: (lim_inf f) . x = (sup (inferior_realsequence f)) . x
hence (lim_inf f) . x = (sup (inferior_realsequence f)) . x by A1, A3, Def4; :: thesis: verum

end;

then for x being Element of X st x in dom (lim_inf f) holds
(lim_inf f) . x = (sup (inferior_realsequence f)) . x ;
hence ( ( 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) ) by A1, A2, PARTFUN1:5; :: thesis: verum