let X be non empty set ; :: thesis: for S being SigmaField of X
for f being Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being natural number holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds
meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r)))
let S be SigmaField of X; :: thesis: for f being Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being natural number holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds
meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r)))
let f be Functional_Sequence of X,ExtREAL; :: thesis: for F being SetSequence of S
for r being real number st ( for n being natural number holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds
meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r)))
let F be SetSequence of S; :: thesis: for r being real number st ( for n being natural number holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds
meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r)))
let r be real number ; :: thesis: ( ( for n being natural number holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) implies meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r))) )
set E = dom (f . 0);
set g = superior_realsequence f;
assume A1: for n being natural number holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ; :: thesis: meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r)))
dom ((superior_realsequence f) . 0) = dom (f . 0) by Def6;
then meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf (superior_realsequence f)),(R_EAL r))) by A1, Th16;
hence meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r))) by Th12; :: thesis: verum