let X1, X2 be non empty set ; for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for E, V being Element of sigma (measurable_rectangles (S1,S2))
for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st P is non-ascending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-ascending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),y)) /\ (Measurable-Y-section (V,y)) ) & lim K = (Measurable-Y-section (E,y)) /\ (Measurable-Y-section (V,y)) )
let S1 be SigmaField of X1; for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for E, V being Element of sigma (measurable_rectangles (S1,S2))
for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st P is non-ascending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-ascending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),y)) /\ (Measurable-Y-section (V,y)) ) & lim K = (Measurable-Y-section (E,y)) /\ (Measurable-Y-section (V,y)) )
let S2 be SigmaField of X2; for M1 being sigma_Measure of S1
for E, V being Element of sigma (measurable_rectangles (S1,S2))
for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st P is non-ascending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-ascending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),y)) /\ (Measurable-Y-section (V,y)) ) & lim K = (Measurable-Y-section (E,y)) /\ (Measurable-Y-section (V,y)) )
let M1 be sigma_Measure of S1; for E, V being Element of sigma (measurable_rectangles (S1,S2))
for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st P is non-ascending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-ascending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),y)) /\ (Measurable-Y-section (V,y)) ) & lim K = (Measurable-Y-section (E,y)) /\ (Measurable-Y-section (V,y)) )
let E, V be Element of sigma (measurable_rectangles (S1,S2)); for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st P is non-ascending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-ascending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),y)) /\ (Measurable-Y-section (V,y)) ) & lim K = (Measurable-Y-section (E,y)) /\ (Measurable-Y-section (V,y)) )
let P be Set_Sequence of sigma (measurable_rectangles (S1,S2)); for y being Element of X2 st P is non-ascending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-ascending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),y)) /\ (Measurable-Y-section (V,y)) ) & lim K = (Measurable-Y-section (E,y)) /\ (Measurable-Y-section (V,y)) )
let x be Element of X2; ( P is non-ascending & lim P = E implies ex K being SetSequence of S1 st
( K is non-ascending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),x)) /\ (Measurable-Y-section (V,x)) ) & lim K = (Measurable-Y-section (E,x)) /\ (Measurable-Y-section (V,x)) ) )
assume that
A1:
P is non-ascending
and
A2:
lim P = E
; ex K being SetSequence of S1 st
( K is non-ascending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),x)) /\ (Measurable-Y-section (V,x)) ) & lim K = (Measurable-Y-section (E,x)) /\ (Measurable-Y-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 X1 such that
A5:
( G is non-ascending & ( for n being Nat holds G . n = Y-section ((P1 . n),x) ) )
by A1, Th40;
for n being Nat holds G . n in S1
then reconsider G = G as Set_Sequence of S1 by MEASURE8:def 2;
set K = (Measurable-Y-section (V,x)) (/\) G;
A6:
( G is convergent & lim G = Intersection G )
by A5, SETLIM_1:64;
meet (rng G) = Y-section ((meet (rng P)),x)
by A5, Th27;
then A7: Intersection G =
Y-section ((meet (rng P)),x)
by SETLIM_1:8
.=
Y-section ((Intersection P),x)
by SETLIM_1:8
.=
Measurable-Y-section (E,x)
by A1, A2, SETLIM_1:64
;
A8:
dom ((Measurable-Y-section (V,x)) (/\) G) = NAT
by FUNCT_2:def 1;
for n being object st n in NAT holds
((Measurable-Y-section (V,x)) (/\) G) . n in S1
then reconsider K = (Measurable-Y-section (V,x)) (/\) G as SetSequence of S1 by A8, FUNCT_2:3;
A9:
for n being Nat holds K . n = (Measurable-Y-section ((P . n),x)) /\ (Measurable-Y-section (V,x))
take
K
; ( K is non-ascending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),x)) /\ (Measurable-Y-section (V,x)) ) & lim K = (Measurable-Y-section (E,x)) /\ (Measurable-Y-section (V,x)) )
thus
( K is non-ascending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),x)) /\ (Measurable-Y-section (V,x)) ) & lim K = (Measurable-Y-section (E,x)) /\ (Measurable-Y-section (V,x)) )
by A9, A7, A6, A5, SETLIM_2:21, SETLIM_2:92; verum