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_sup f) holds
( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) ) & lim_sup f = inf (superior_realsequence f) )
let f be Functional_Sequence of X,ExtREAL ; :: thesis: ( ( for x being Element of X st x in dom (lim_sup f) holds
( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) ) & lim_sup f = inf (superior_realsequence f) )
A1: dom (inf (superior_realsequence f)) = dom ((superior_realsequence f) . 0 ) by Def3
.= dom (f . 0 ) by Def6
.= dom (lim_sup f) by Def9 ;

A2: now

let x be Element of X; :: thesis: ( x in dom (lim_sup f) implies ( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) )
assume A3: x in dom (lim_sup f) ; :: thesis: ( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x )
then A4: (lim_sup f) . x = lim_sup (f # x) by Def9;
hence (lim_sup f) . x = inf (superior_realsequence (f # x)) ; :: thesis: ( (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x )
dom (lim_sup f) = dom (f . 0 ) by Def9;
hence (lim_sup f) . x = inf ((superior_realsequence f) # x) by A3, A4, Th10; :: thesis: (lim_sup f) . x = (inf (superior_realsequence f)) . x
hence (lim_sup f) . x = (inf (superior_realsequence f)) . x by A1, A3, Def3; :: thesis: verum

end;

then for x being Element of X st x in dom (lim_sup f) holds
(lim_sup f) . x = (inf (superior_realsequence f)) . x ;
hence ( ( for x being Element of X st x in dom (lim_sup f) holds
( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) ) & lim_sup f = inf (superior_realsequence f) ) by A1, A2, PARTFUN1:34; :: thesis: verum