let X be non empty set ; :: thesis: 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 number st ( for n being natural number holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
for n being natural number holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r)))
let S be SigmaField of X; :: thesis: for f being with_the_same_dom 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 ((f . n),(R_EAL r))) ) holds
for n being natural number holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r)))
let f be with_the_same_dom 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 ((f . n),(R_EAL r))) ) holds
for n being natural number holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(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 ((f . n),(R_EAL r))) ) holds
for n being natural number holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r)))
let r be real number ; :: thesis: ( ( for n being natural number holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) implies for n being natural number holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) )
set E = dom (f . 0);
assume A1: for n being natural number holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ; :: thesis: for n being natural number holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r)))
let n be natural number ; :: thesis: (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r)))
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
set f1 = f ^\ n9;
set F1 = F ^\ n9;

A2: now

let k be natural number ; :: thesis: (F ^\ n9) . k = (dom (f . 0)) /\ (great_dom (((f ^\ n9) . k),(R_EAL r)))
reconsider k9 = k as Element of NAT by ORDINAL1:def 12;
(F ^\ n9) . k = F . (n + k9) by NAT_1:def 3;
then (F ^\ n9) . k = (dom (f . 0)) /\ (great_dom ((f . (n + k9)),(R_EAL r))) by A1;
hence (F ^\ n9) . k = (dom (f . 0)) /\ (great_dom (((f ^\ n9) . k),(R_EAL r))) by NAT_1:def 3; :: thesis: verum

end;

A3: union (rng (F ^\ n9)) = (superior_setsequence F) . n by Th2;

now

let k be Nat; :: thesis: (F ^\ n9) . k in S
A4: F . (n + k) in rng F by NAT_1:51;
A5: (F ^\ n9) . k = F . (n + k) by NAT_1:def 3;
rng F c= S by RELAT_1:def 19;
hence (F ^\ n9) . k in S by A4, A5; :: thesis: verum

end;

then rng (F ^\ n9) c= S by NAT_1:52;
then A6: F ^\ n9 is SetSequence of S by RELAT_1:def 19;
consider g being Function of NAT,(PFuncs (X,ExtREAL)) such that
A7: f = g and
f ^\ n9 = g ^\ n9 ;
(f ^\ n9) . 0 = g . (n + 0) by A7, NAT_1:def 3;
then dom ((f ^\ n9) . 0) = dom (f . 0) by A7, Def2;
then union (rng (F ^\ n9)) = (dom (f . 0)) /\ (great_dom ((sup (f ^\ n9)),(R_EAL r))) by A6, A2, Th15;
hence (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) by A3, Th9; :: thesis: verum