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 M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for V being Element of S1 st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
ex F being Function of X2,ExtREAL st
( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) )
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for V being Element of S1 st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
ex F being Function of X2,ExtREAL st
( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) )
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for V being Element of S1 st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
ex F being Function of X2,ExtREAL st
( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) )
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for V being Element of S1 st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
ex F being Function of X2,ExtREAL st
( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) )
let M2 be sigma_Measure of S2; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2))
for V being Element of S1 st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
ex F being Function of X2,ExtREAL st
( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) )
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: for V being Element of S1 st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
ex F being Function of X2,ExtREAL st
( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) )
let V be Element of S1; :: thesis: ( E in Field_generated_by (measurable_rectangles (S1,S2)) implies ex F being Function of X2,ExtREAL st
( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) ) )
assume A1: E in Field_generated_by (measurable_rectangles (S1,S2)) ; :: thesis: ex F being Function of X2,ExtREAL st
( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) )
X2 in S2 by MEASURE1:7;
then [:V,X2:] in { [:A,B:] where A is Element of S1, B is Element of S2 : verum } ;
then A2: [:V,X2:] in measurable_rectangles (S1,S2) by MEASUR10:def 5;
measurable_rectangles (S1,S2) c= sigma (measurable_rectangles (S1,S2)) by PROB_1:def 9;
then reconsider E1 = E /\ [:V,X2:] as Element of sigma (measurable_rectangles (S1,S2)) by A2, FINSUB_1:def 2;
A3: measurable_rectangles (S1,S2) c= Field_generated_by (measurable_rectangles (S1,S2)) by SRINGS_3:21;

per cases ( E1 = {} or E1 <> {} ) ;

suppose A4: E1 = {} ; :: thesis: ex F being Function of X2,ExtREAL st
( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) )

reconsider A = {} as Element of S2 by MEASURE1:34;
0 in REAL by XREAL_0:def 1;
then reconsider F = X2 --> 0 as Function of X2,ExtREAL by FUNCOP_1:45, NUMBERS:31;
take F ; :: thesis: ( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) )
thus for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) :: thesis: for P being Element of S2 holds F is P -measurable

proof

let x be Element of X2; :: thesis: F . x = M1 . ((Measurable-Y-section (E,x)) /\ V)
A5: X2 = [#] X2 by SUBSET_1:def 3;
(Measurable-Y-section (E,x)) /\ V = (Y-section (E,x)) /\ (Y-section ([:V,([#] X2):],x)) by A5, Th16
.= Y-section (({} [:X1,X2:]),x) by A4, A5, Th21
.= {} ;
then M1 . ((Measurable-Y-section (E,x)) /\ V) = 0 by VALUED_0:def 19;
hence F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) by FUNCOP_1:7; :: thesis: verum

end;

thus for P being Element of S2 holds F is P -measurable :: thesis: verum

proof

let P be Element of S2; :: thesis: F is P -measurable
for x being Element of X2 holds F . x = (chi ({},X2)) . x

proof

let x be Element of X2; :: thesis: F . x = (chi ({},X2)) . x
(chi ({},X2)) . x = 0 by FUNCT_3:def 3;
hence F . x = (chi ({},X2)) . x by FUNCOP_1:7; :: thesis: verum

end;

then F = chi (A,X2) by FUNCT_2:def 8;
hence F is P -measurable by MESFUNC2:29; :: thesis: verum

end;

end;

suppose A6: E1 <> {} ; :: thesis: ex F being Function of X2,ExtREAL st
( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) )

deffunc H₁( Element of X2) -> Element of ExtREAL = M1 . ((Measurable-Y-section (E,$1)) /\ V);
consider F being Function of X2,ExtREAL such that
A7: for x being Element of X2 holds F . x = H₁(x) from FUNCT_2:sch 4();
consider f being disjoint_valued FinSequence of measurable_rectangles (S1,S2), A being FinSequence of S1, B being FinSequence of S2, Xf being summable FinSequence of Funcs ([:X1,X2:],ExtREAL), If being summable FinSequence of Funcs (X1,ExtREAL), Jf being summable FinSequence of Funcs (X2,ExtREAL) such that
A8: ( E /\ [:V,X2:] = Union f & len f in dom f & len f = len A & len f = len B & len f = len Xf & len f = len If & len f = len Jf & ( for n being Nat st n in dom Xf holds
Xf . n = chi ((f . n),[:X1,X2:]) ) & (Partial_Sums Xf) /. (len Xf) = chi ((E /\ [:V,X2:]),[:X1,X2:]) & ( for x being Element of X1
for n being Nat st n in dom If holds
(If . n) . x = Integral (M2,(ProjMap1 ((Xf /. n),x))) ) & ( for n being Nat
for P being Element of S1 st n in dom If holds
If /. n is P -measurable ) & ( for x being Element of X1 holds Integral (M2,(ProjMap1 (((Partial_Sums Xf) /. (len Xf)),x))) = ((Partial_Sums If) /. (len If)) . x ) & ( for x being Element of X2
for n being Nat st n in dom Jf holds
(Jf . n) . x = Integral (M1,(ProjMap2 ((Xf /. n),x))) ) & ( for n being Nat
for P being Element of S2 st n in dom Jf holds
Jf /. n is P -measurable ) & ( for x being Element of X2 holds Integral (M1,(ProjMap2 (((Partial_Sums Xf) /. (len Xf)),x))) = ((Partial_Sums Jf) /. (len Jf)) . x ) ) by A3, A1, A2, FINSUB_1:def 2, A6, Th75;
take F ; :: thesis: ( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) )
thus for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) by A7; :: thesis: for P being Element of S2 holds F is P -measurable
A9: dom Jf = dom f by A8, FINSEQ_3:29;
for x being Element of X2 holds F . x = ((Partial_Sums Jf) /. (len Jf)) . x

proof

let x be Element of X2; :: thesis: F . x = ((Partial_Sums Jf) /. (len Jf)) . x
((Partial_Sums Jf) /. (len Jf)) . x = Integral (M1,(ProjMap2 ((chi ((E /\ [:V,X2:]),[:X1,X2:])),x))) by A8
.= M1 . ((Measurable-Y-section (E,x)) /\ V) by Th67 ;
hence F . x = ((Partial_Sums Jf) /. (len Jf)) . x by A7; :: thesis: verum

end;

then A10: F = (Partial_Sums Jf) /. (len Jf) by FUNCT_2:def 8;
let P be Element of S2; :: thesis: F is P -measurable
for n being Nat st n in dom Jf holds
Jf /. n is P -measurable by A8;
hence F is P -measurable by A8, A9, A10, Th64; :: thesis: verum

end;

end;