let X1, X2 be non empty set ; for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for E, V being Element of sigma (measurable_rectangles (S1,S2))
for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for x being Element of X1 st P is non-descending & lim P = E holds
ex K being SetSequence of S2 st
( K is non-descending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )
let S1 be SigmaField of X1; for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for E, V being Element of sigma (measurable_rectangles (S1,S2))
for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for x being Element of X1 st P is non-descending & lim P = E holds
ex K being SetSequence of S2 st
( K is non-descending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )
let S2 be SigmaField of X2; for M2 being sigma_Measure of S2
for E, V being Element of sigma (measurable_rectangles (S1,S2))
for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for x being Element of X1 st P is non-descending & lim P = E holds
ex K being SetSequence of S2 st
( K is non-descending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )
let M2 be sigma_Measure of S2; for E, V being Element of sigma (measurable_rectangles (S1,S2))
for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for x being Element of X1 st P is non-descending & lim P = E holds
ex K being SetSequence of S2 st
( K is non-descending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )
let E, V be Element of sigma (measurable_rectangles (S1,S2)); for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for x being Element of X1 st P is non-descending & lim P = E holds
ex K being SetSequence of S2 st
( K is non-descending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )
let P be Set_Sequence of sigma (measurable_rectangles (S1,S2)); for x being Element of X1 st P is non-descending & lim P = E holds
ex K being SetSequence of S2 st
( K is non-descending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )
let x be Element of X1; ( P is non-descending & lim P = E implies ex K being SetSequence of S2 st
( K is non-descending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) ) )
assume that
A1:
P is non-descending
and
A2:
lim P = E
; ex K being SetSequence of S2 st
( K is non-descending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )
A4:
for n being Nat holds P . n in sigma (measurable_rectangles (S1,S2))
;
reconsider P1 = P as SetSequence of [:X1,X2:] ;
consider G being SetSequence of X2 such that
A5:
( G is non-descending & ( for n being Nat holds G . n = X-section ((P1 . n),x) ) )
by A1, Th37;
for n being Nat holds G . n in S2
then reconsider G = G as Set_Sequence of S2 by MEASURE8:def 2;
set K = (Measurable-X-section (V,x)) (/\) G;
A6:
( G is convergent & lim G = Union G )
by A5, SETLIM_1:63;
union (rng G) = X-section ((union (rng P)),x)
by A5, Th24;
then A7: Union G =
X-section ((union (rng P)),x)
by CARD_3:def 4
.=
X-section ((Union P),x)
by CARD_3:def 4
.=
Measurable-X-section (E,x)
by A1, A2, SETLIM_1:63
;
A8:
dom ((Measurable-X-section (V,x)) (/\) G) = NAT
by FUNCT_2:def 1;
for n being object st n in NAT holds
((Measurable-X-section (V,x)) (/\) G) . n in S2
then reconsider K = (Measurable-X-section (V,x)) (/\) G as SetSequence of S2 by A8, FUNCT_2:3;
A9:
for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x))
take
K
; ( K is non-descending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )
thus
( K is non-descending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )
by A9, A7, A6, A5, SETLIM_2:22, SETLIM_2:92; verum