let X1, X2 be non empty set ; :: thesis: 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-descending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-descending & ( 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; :: thesis: 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-descending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-descending & ( 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; :: thesis: 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-descending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-descending & ( 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; :: thesis: 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-descending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-descending & ( 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)); :: thesis: for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st P is non-descending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-descending & ( 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)); :: thesis: for y being Element of X2 st P is non-descending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-descending & ( 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; :: thesis: ( P is non-descending & lim P = E implies ex K being SetSequence of S1 st
( K is non-descending & ( 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-descending and
A2: lim P = E ; :: thesis: ex K being SetSequence of S1 st
( K is non-descending & ( 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-descending & ( for n being Nat holds G . n = Y-section ((P1 . n),x) ) ) by A1, Th38;
for n being Nat holds G . n in S1

proof

let n be Nat; :: thesis: G . n in S1
P1 . n in sigma (measurable_rectangles (S1,S2)) by A4;
then Y-section ((P1 . n),x) in S1 by Th44;
hence G . n in S1 by A5; :: thesis: verum

end;

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 = Union G ) by A5, SETLIM_1:63;
union (rng G) = Y-section ((union (rng P)),x) by A5, Th26;
then A7: Union G = Y-section ((union (rng P)),x) by CARD_3:def 4
.= Y-section ((Union P),x) by CARD_3:def 4
.= Measurable-Y-section (E,x) by A1, A2, SETLIM_1:63 ;
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

proof

let n be object ; :: thesis: ( n in NAT implies ((Measurable-Y-section (V,x)) (/\) G) . n in S1 )
assume n in NAT ; :: thesis: ((Measurable-Y-section (V,x)) (/\) G) . n in S1
then reconsider n1 = n as Element of NAT ;
((Measurable-Y-section (V,x)) (/\) G) . n1 = (G . n1) /\ (Measurable-Y-section (V,x)) by SETLIM_2:def 5;
then ((Measurable-Y-section (V,x)) (/\) G) . n1 = (Measurable-Y-section ((P . n1),x)) /\ (Measurable-Y-section (V,x)) by A5;
hence ((Measurable-Y-section (V,x)) (/\) G) . n in S1 ; :: thesis: verum

end;

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))

proof

let n be Nat; :: thesis: K . n = (Measurable-Y-section ((P . n),x)) /\ (Measurable-Y-section (V,x))
K . n = (G . n) /\ (Measurable-Y-section (V,x)) by SETLIM_2:def 5;
hence K . n = (Measurable-Y-section ((P . n),x)) /\ (Measurable-Y-section (V,x)) by A5; :: thesis: verum

end;

take K ; :: thesis: ( K is non-descending & ( 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-descending & ( 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, A5, A6, SETLIM_2:22, SETLIM_2:92; :: thesis: verum