let X be non empty set ; for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),r))
let S be SigmaField of X; for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),r))
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; for F being SetSequence of S
for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),r))
let F be SetSequence of S; for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),r))
let r be Real; ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) implies for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),r)) )
set E = dom (f . 0);
assume A1:
for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r))
; for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),r))
let n be Nat; (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),r))
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
set f1 = f ^\ n9;
set F1 = F ^\ n9;
A3:
meet (rng (F ^\ n9)) = (inferior_setsequence F) . n
by Th2;
consider g being sequence of (PFuncs (X,ExtREAL)) such that
A4:
f = g
and
f ^\ n9 = g ^\ n9
;
(f ^\ n9) . 0 = g . (n + 0)
by A4, NAT_1:def 3;
then
dom ((f ^\ n9) . 0) = dom (f . 0)
by A4, Def2;
then
meet (rng (F ^\ n9)) = (dom (f . 0)) /\ (great_eq_dom ((inf (f ^\ n9)),r))
by A2, Th16;
hence
(inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),r))
by A3, Th8; verum