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_sup f) holds
(lim_sup f) . x = lim_sup (R_EAL (f # x))
let f be Functional_Sequence of X,REAL; :: thesis: for x being Element of X st x in dom (lim_sup f) holds
(lim_sup f) . x = lim_sup (R_EAL (f # x))
let x be Element of X; :: thesis: ( x in dom (lim_sup f) implies (lim_sup f) . x = lim_sup (R_EAL (f # x)) )
assume x in dom (lim_sup f) ; :: thesis: (lim_sup f) . x = lim_sup (R_EAL (f # x))
then (lim_sup f) . x = lim_sup ((R_EAL f) # x) by MESFUNC8:def 8;
hence (lim_sup f) . x = lim_sup (R_EAL (f # x)) by Th1; :: thesis: verum