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_dom ((inferior_realsequence f) . n),(R_EAL r)) ) holds
union (rng F) = (dom (f . 0 )) /\ (great_dom (lim_inf 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_dom ((inferior_realsequence f) . n),(R_EAL r)) ) holds
union (rng F) = (dom (f . 0 )) /\ (great_dom (lim_inf 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_dom ((inferior_realsequence f) . n),(R_EAL r)) ) holds
union (rng F) = (dom (f . 0 )) /\ (great_dom (lim_inf 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_dom ((inferior_realsequence f) . n),(R_EAL r)) ) holds
union (rng F) = (dom (f . 0 )) /\ (great_dom (lim_inf f),(R_EAL r))
let r be real number ; :: thesis: ( ( for n being natural number holds F . n = (dom (f . 0 )) /\ (great_dom ((inferior_realsequence f) . n),(R_EAL r)) ) implies union (rng F) = (dom (f . 0 )) /\ (great_dom (lim_inf f),(R_EAL r)) )
set E = dom (f . 0 );
set g = inferior_realsequence f;
assume A1: for n being natural number holds F . n = (dom (f . 0 )) /\ (great_dom ((inferior_realsequence f) . n),(R_EAL r)) ; :: thesis: union (rng F) = (dom (f . 0 )) /\ (great_dom (lim_inf f),(R_EAL r))
dom ((inferior_realsequence f) . 0 ) = dom (f . 0 ) by Def5;
then union (rng F) = (dom (f . 0 )) /\ (great_dom (sup (inferior_realsequence f)),(R_EAL r)) by A1, Th15;
hence union (rng F) = (dom (f . 0 )) /\ (great_dom (lim_inf f),(R_EAL r)) by Th11; :: thesis: verum