let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for x being Element of X1
for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL st f is_simple_func_in sigma (measurable_rectangles (S1,S2)) holds
( ProjPMap1 (f,x) is_simple_func_in S2 & ProjPMap2 (f,y) is_simple_func_in S1 )
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for x being Element of X1
for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL st f is_simple_func_in sigma (measurable_rectangles (S1,S2)) holds
( ProjPMap1 (f,x) is_simple_func_in S2 & ProjPMap2 (f,y) is_simple_func_in S1 )
let S2 be SigmaField of X2; :: thesis: for x being Element of X1
for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL st f is_simple_func_in sigma (measurable_rectangles (S1,S2)) holds
( ProjPMap1 (f,x) is_simple_func_in S2 & ProjPMap2 (f,y) is_simple_func_in S1 )
let x be Element of X1; :: thesis: for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL st f is_simple_func_in sigma (measurable_rectangles (S1,S2)) holds
( ProjPMap1 (f,x) is_simple_func_in S2 & ProjPMap2 (f,y) is_simple_func_in S1 )
let y be Element of X2; :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL st f is_simple_func_in sigma (measurable_rectangles (S1,S2)) holds
( ProjPMap1 (f,x) is_simple_func_in S2 & ProjPMap2 (f,y) is_simple_func_in S1 )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: ( f is_simple_func_in sigma (measurable_rectangles (S1,S2)) implies ( ProjPMap1 (f,x) is_simple_func_in S2 & ProjPMap2 (f,y) is_simple_func_in S1 ) )
assume AS: f is_simple_func_in sigma (measurable_rectangles (S1,S2)) ; :: thesis: ( ProjPMap1 (f,x) is_simple_func_in S2 & ProjPMap2 (f,y) is_simple_func_in S1 )
then A1: ( f is real-valued & ex F being Finite_Sep_Sequence of sigma (measurable_rectangles (S1,S2)) st
( dom f = union (rng F) & ( for n being Nat
for x, y being Element of [:X1,X2:] st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) ) ) by MESFUNC2:def 4;
consider F being Finite_Sep_Sequence of sigma (measurable_rectangles (S1,S2)) such that
A2: dom f = union (rng F) and
A3: for n being Nat
for z1, z2 being Element of [:X1,X2:] st n in dom F & z1 in F . n & z2 in F . n holds
f . z1 = f . z2 by AS, MESFUNC2:def 4;
A4: rng f c= REAL by A1, VALUED_0:def 3;

now :: thesis: for a being object st a in rng (ProjPMap1 (f,x)) holds
a in REAL

let a be object ; :: thesis: ( a in rng (ProjPMap1 (f,x)) implies a in REAL )
assume a in rng (ProjPMap1 (f,x)) ; :: thesis: a in REAL
then consider y1 being Element of X2 such that
A5: ( y1 in dom (ProjPMap1 (f,x)) & a = (ProjPMap1 (f,x)) . y1 ) by PARTFUN1:3;
A6: a = f . (x,y1) by A5, Th26;
y1 in X-section ((dom f),x) by A5, Def3;
then y1 in { y where y is Element of X2 : [x,y] in dom f } by MEASUR11:def 4;
then ex y being Element of X2 st
( y1 = y & [x,y] in dom f ) ;
hence a in REAL by A4, A6, FUNCT_1:3; :: thesis: verum

end;

then rng (ProjPMap1 (f,x)) c= REAL ;
then A7: ProjPMap1 (f,x) is real-valued by VALUED_0:def 3;
deffunc H₁( Nat) -> Element of S2 = Measurable-X-section ((F . $1),x);
consider F1 being FinSequence of S2 such that
A8: ( len F1 = len F & ( for n being Nat st n in dom F1 holds
F1 . n = H₁(n) ) ) from FINSEQ_2:sch 1();
A9: dom F1 = dom F by A8, FINSEQ_3:29;
reconsider FF = F as FinSequence of bool [:X1,X2:] by FINSEQ_2:24;

now :: thesis: for m, n being Nat st m in dom F1 & n in dom F1 & m <> n holds
F1 . m misses F1 . n

let m, n be Nat; :: thesis: ( m in dom F1 & n in dom F1 & m <> n implies F1 . m misses F1 . n )
assume A10: ( m in dom F1 & n in dom F1 & m <> n ) ; :: thesis: F1 . m misses F1 . n
( Measurable-X-section ((F . m),x) = X-section ((F . m),x) & Measurable-X-section ((F . n),x) = X-section ((F . n),x) ) by MEASUR11:def 6;
then A11: ( F1 . m = X-section ((F . m),x) & F1 . n = X-section ((F . n),x) ) by A10, A8;
F . m misses F . n by A9, A10, Def2;
hence F1 . m misses F1 . n by A11, MEASUR11:35; :: thesis: verum

end;

then F1 is disjoint_valued ;
then reconsider F1 = F1 as Finite_Sep_Sequence of S2 ;
reconsider FF1 = F1 as FinSequence of bool X2 by FINSEQ_2:24;
A12: for n being Nat st n in dom FF1 holds
FF1 . n = X-section ((FF . n),x)

proof

let n be Nat; :: thesis: ( n in dom FF1 implies FF1 . n = X-section ((FF . n),x) )
assume n in dom FF1 ; :: thesis: FF1 . n = X-section ((FF . n),x)
then FF1 . n = Measurable-X-section ((F . n),x) by A8;
hence FF1 . n = X-section ((FF . n),x) by MEASUR11:def 6; :: thesis: verum

end;

then X-section ((union (rng FF)),x) = union (rng FF1) by A9, MEASUR11:28;
then A13: dom (ProjPMap1 (f,x)) = union (rng F1) by A2, Def3;
for n being Nat
for y1, y2 being Element of X2 st n in dom F1 & y1 in F1 . n & y2 in F1 . n holds
(ProjPMap1 (f,x)) . y1 = (ProjPMap1 (f,x)) . y2

proof

let n be Nat; :: thesis: for y1, y2 being Element of X2 st n in dom F1 & y1 in F1 . n & y2 in F1 . n holds
(ProjPMap1 (f,x)) . y1 = (ProjPMap1 (f,x)) . y2
let y1, y2 be Element of X2; :: thesis: ( n in dom F1 & y1 in F1 . n & y2 in F1 . n implies (ProjPMap1 (f,x)) . y1 = (ProjPMap1 (f,x)) . y2 )
assume A14: ( n in dom F1 & y1 in F1 . n & y2 in F1 . n ) ; :: thesis: (ProjPMap1 (f,x)) . y1 = (ProjPMap1 (f,x)) . y2
then A15: F1 . n = X-section ((FF . n),x) by A12;
A17: FF . n in rng F by A9, A14, FUNCT_1:3;
then FF . n c= union (rng F) by TARSKI:def 4;
then F1 . n c= X-section ((dom f),x) by A2, A15, MEASUR11:20;
then ( y1 in X-section ((dom f),x) & y2 in X-section ((dom f),x) ) by A14;
then ( y1 in dom (ProjPMap1 (f,x)) & y2 in dom (ProjPMap1 (f,x)) ) by Def3;
then A16: ( (ProjPMap1 (f,x)) . y1 = f . (x,y1) & (ProjPMap1 (f,x)) . y2 = f . (x,y2) ) by Th26;
A18: ( [x,y1] in union (rng F) implies [x,y1] in F . n )

proof

assume [x,y1] in union (rng F) ; :: thesis: [x,y1] in F . n
then consider A being set such that
A19: ( [x,y1] in A & A in rng F ) by TARSKI:def 4;
consider m being object such that
A20: ( m in dom F & A = F . m ) by A19, FUNCT_1:def 3;
reconsider m = m as Nat by A20;

now :: thesis: not m <> n

assume m <> n ; :: thesis: contradiction
then for y being Element of X2 st y1 = y holds
not [x,y] in F . n by A19, A20, XBOOLE_0:3, PROB_2:def 2;
then not y1 in { y where y is Element of X2 : [x,y] in F . n } ;
then not y1 in X-section ((F . n),x) by MEASUR11:def 4;
hence contradiction by A14, A12; :: thesis: verum

end;

hence [x,y1] in F . n by A19, A20; :: thesis: verum

end;

A21: [x,y1] in union (rng F)

proof

assume not [x,y1] in union (rng F) ; :: thesis: contradiction
then for y being Element of X2 st y1 = y holds
not [x,y] in F . n by A17, TARSKI:def 4;
then not y1 in { y where y is Element of X2 : [x,y] in F . n } ;
then not y1 in X-section ((F . n),x) by MEASUR11:def 4;
hence contradiction by A14, A12; :: thesis: verum

end;

now :: thesis: [x,y2] in F . n

assume not [x,y2] in F . n ; :: thesis: contradiction
then for y being Element of X2 st y2 = y holds
not [x,y] in F . n ;
then not y2 in { y where y is Element of X2 : [x,y] in F . n } ;
then not y2 in X-section ((F . n),x) by MEASUR11:def 4;
hence contradiction by A14, A12; :: thesis: verum

end;

hence (ProjPMap1 (f,x)) . y1 = (ProjPMap1 (f,x)) . y2 by A3, A14, A9, A16, A18, A21; :: thesis: verum

end;

hence ProjPMap1 (f,x) is_simple_func_in S2 by A7, A13, MESFUNC2:def 4; :: thesis: ProjPMap2 (f,y) is_simple_func_in S1

now :: thesis: for a being object st a in rng (ProjPMap2 (f,y)) holds
a in REAL

let a be object ; :: thesis: ( a in rng (ProjPMap2 (f,y)) implies a in REAL )
assume a in rng (ProjPMap2 (f,y)) ; :: thesis: a in REAL
then consider x1 being Element of X1 such that
A25: ( x1 in dom (ProjPMap2 (f,y)) & a = (ProjPMap2 (f,y)) . x1 ) by PARTFUN1:3;
A26: a = f . (x1,y) by A25, Th26;
x1 in Y-section ((dom f),y) by A25, Def4;
then x1 in { x where x is Element of X1 : [x,y] in dom f } by MEASUR11:def 5;
then ex x being Element of X1 st
( x1 = x & [x,y] in dom f ) ;
hence a in REAL by A4, A26, FUNCT_1:3; :: thesis: verum

end;

then rng (ProjPMap2 (f,y)) c= REAL ;
then A27: ProjPMap2 (f,y) is real-valued by VALUED_0:def 3;
deffunc H₂( Nat) -> Element of S1 = Measurable-Y-section ((F . $1),y);
consider G1 being FinSequence of S1 such that
A28: ( len G1 = len F & ( for n being Nat st n in dom G1 holds
G1 . n = H₂(n) ) ) from FINSEQ_2:sch 1();
A29: dom G1 = dom F by A28, FINSEQ_3:29;

now :: thesis: for m, n being Nat st m in dom G1 & n in dom G1 & m <> n holds
G1 . m misses G1 . n

let m, n be Nat; :: thesis: ( m in dom G1 & n in dom G1 & m <> n implies G1 . m misses G1 . n )
assume A30: ( m in dom G1 & n in dom G1 & m <> n ) ; :: thesis: G1 . m misses G1 . n
( Measurable-Y-section ((F . m),y) = Y-section ((F . m),y) & Measurable-Y-section ((F . n),y) = Y-section ((F . n),y) ) by MEASUR11:def 7;
then A31: ( G1 . m = Y-section ((F . m),y) & G1 . n = Y-section ((F . n),y) ) by A30, A28;
F . m misses F . n by A29, A30, Def2;
hence G1 . m misses G1 . n by A31, MEASUR11:35; :: thesis: verum

end;

then G1 is disjoint_valued ;
then reconsider G1 = G1 as Finite_Sep_Sequence of S1 ;
reconsider GG1 = G1 as FinSequence of bool X1 by FINSEQ_2:24;
A32: for n being Nat st n in dom GG1 holds
GG1 . n = Y-section ((FF . n),y)

proof

let n be Nat; :: thesis: ( n in dom GG1 implies GG1 . n = Y-section ((FF . n),y) )
assume n in dom GG1 ; :: thesis: GG1 . n = Y-section ((FF . n),y)
then GG1 . n = Measurable-Y-section ((F . n),y) by A28;
hence GG1 . n = Y-section ((FF . n),y) by MEASUR11:def 7; :: thesis: verum

end;

then Y-section ((union (rng FF)),y) = union (rng GG1) by A29, MEASUR11:29;
then A33: dom (ProjPMap2 (f,y)) = union (rng G1) by A2, Def4;
for n being Nat
for x1, x2 being Element of X1 st n in dom G1 & x1 in G1 . n & x2 in G1 . n holds
(ProjPMap2 (f,y)) . x1 = (ProjPMap2 (f,y)) . x2

proof

let n be Nat; :: thesis: for x1, x2 being Element of X1 st n in dom G1 & x1 in G1 . n & x2 in G1 . n holds
(ProjPMap2 (f,y)) . x1 = (ProjPMap2 (f,y)) . x2
let x1, x2 be Element of X1; :: thesis: ( n in dom G1 & x1 in G1 . n & x2 in G1 . n implies (ProjPMap2 (f,y)) . x1 = (ProjPMap2 (f,y)) . x2 )
assume A34: ( n in dom G1 & x1 in G1 . n & x2 in G1 . n ) ; :: thesis: (ProjPMap2 (f,y)) . x1 = (ProjPMap2 (f,y)) . x2
then A35: G1 . n = Y-section ((FF . n),y) by A32;
A37: FF . n in rng F by A29, A34, FUNCT_1:3;
then FF . n c= union (rng F) by TARSKI:def 4;
then G1 . n c= Y-section ((dom f),y) by A2, A35, MEASUR11:21;
then ( x1 in Y-section ((dom f),y) & x2 in Y-section ((dom f),y) ) by A34;
then ( x1 in dom (ProjPMap2 (f,y)) & x2 in dom (ProjPMap2 (f,y)) ) by Def4;
then A36: ( (ProjPMap2 (f,y)) . x1 = f . (x1,y) & (ProjPMap2 (f,y)) . x2 = f . (x2,y) ) by Th26;
A38: ( [x1,y] in union (rng F) implies [x1,y] in F . n )

proof

assume [x1,y] in union (rng F) ; :: thesis: [x1,y] in F . n
then consider A being set such that
A39: ( [x1,y] in A & A in rng F ) by TARSKI:def 4;
consider m being object such that
A40: ( m in dom F & A = F . m ) by A39, FUNCT_1:def 3;
reconsider m = m as Nat by A40;

now :: thesis: not m <> n

assume m <> n ; :: thesis: contradiction
then for x being Element of X1 st x1 = x holds
not [x,y] in F . n by A39, A40, XBOOLE_0:3, PROB_2:def 2;
then not x1 in { x where x is Element of X1 : [x,y] in F . n } ;
then not x1 in Y-section ((F . n),y) by MEASUR11:def 5;
hence contradiction by A34, A32; :: thesis: verum

end;

hence [x1,y] in F . n by A39, A40; :: thesis: verum

end;

A41: [x1,y] in union (rng F)

proof

assume not [x1,y] in union (rng F) ; :: thesis: contradiction
then for x being Element of X1 st x1 = x holds
not [x,y] in F . n by A37, TARSKI:def 4;
then not x1 in { x where x is Element of X1 : [x,y] in F . n } ;
then not x1 in Y-section ((F . n),y) by MEASUR11:def 5;
hence contradiction by A34, A32; :: thesis: verum

end;

now :: thesis: [x2,y] in F . n

assume not [x2,y] in F . n ; :: thesis: contradiction
then for x being Element of X1 st x2 = x holds
not [x,y] in F . n ;
then not x2 in { x where x is Element of X1 : [x,y] in F . n } ;
then not x2 in Y-section ((F . n),y) by MEASUR11:def 5;
hence contradiction by A34, A32; :: thesis: verum

end;

hence (ProjPMap2 (f,y)) . x1 = (ProjPMap2 (f,y)) . x2 by A3, A34, A29, A36, A38, A41; :: thesis: verum

end;

hence ProjPMap2 (f,y) is_simple_func_in S1 by A27, A33, MESFUNC2:def 4; :: thesis: verum