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
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
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
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 ; :: 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 n' = n as Element of NAT by ORDINAL1:def 13;
set f1 = f ^\ n';
set F1 = F ^\ n';

now

let k be Nat; :: thesis: (F ^\ n') . k in S
X: rng F c= S by RELAT_1:def 19;
Y: F . (n + k) in rng F by NAT_1:52;
(F ^\ n') . k = F . (n + k) by NAT_1:def 3;
hence (F ^\ n') . k in S by X, Y; :: thesis: verum

end;

then rng (F ^\ n') c= S by NAT_1:53;
then A2: F ^\ n' is SetSequence of by RELAT_1:def 19;
consider g being Function of NAT ,(PFuncs X,ExtREAL ) such that
A3: ( f = g & f ^\ n' = g ^\ n' ) ;
(f ^\ n') . 0 = g . (n + 0 ) by A3, NAT_1:def 3;
then A4: dom ((f ^\ n') . 0 ) = dom (f . 0 ) by A3, Def2;

now

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

end;

then A5: union (rng (F ^\ n')) = (dom (f . 0 )) /\ (great_dom (sup (f ^\ n')),(R_EAL r)) by A2, A4, Th15;
union (rng (F ^\ n')) = (superior_setsequence F) . n by Th2;
hence (superior_setsequence F) . n = (dom (f . 0 )) /\ (great_dom ((superior_realsequence f) . n),(R_EAL r)) by A5, Th9; :: thesis: verum