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 M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonpositive & f is E1 -measurable holds
( Integral1 (M1,f) is nonpositive & Integral1 (M1,(f | E2)) is nonpositive & Integral2 (M2,f) is nonpositive & Integral2 (M2,(f | E2)) is nonpositive )
let S1 be SigmaField of X1; for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonpositive & f is E1 -measurable holds
( Integral1 (M1,f) is nonpositive & Integral1 (M1,(f | E2)) is nonpositive & Integral2 (M2,f) is nonpositive & Integral2 (M2,(f | E2)) is nonpositive )
let S2 be SigmaField of X2; for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonpositive & f is E1 -measurable holds
( Integral1 (M1,f) is nonpositive & Integral1 (M1,(f | E2)) is nonpositive & Integral2 (M2,f) is nonpositive & Integral2 (M2,(f | E2)) is nonpositive )
let M1 be sigma_Measure of S1; for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonpositive & f is E1 -measurable holds
( Integral1 (M1,f) is nonpositive & Integral1 (M1,(f | E2)) is nonpositive & Integral2 (M2,f) is nonpositive & Integral2 (M2,(f | E2)) is nonpositive )
let M2 be sigma_Measure of S2; for f being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonpositive & f is E1 -measurable holds
( Integral1 (M1,f) is nonpositive & Integral1 (M1,(f | E2)) is nonpositive & Integral2 (M2,f) is nonpositive & Integral2 (M2,(f | E2)) is nonpositive )
let f be PartFunc of [:X1,X2:],ExtREAL; for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonpositive & f is E1 -measurable holds
( Integral1 (M1,f) is nonpositive & Integral1 (M1,(f | E2)) is nonpositive & Integral2 (M2,f) is nonpositive & Integral2 (M2,(f | E2)) is nonpositive )
let A, B be Element of sigma (measurable_rectangles (S1,S2)); ( A = dom f & f is nonpositive & f is A -measurable implies ( Integral1 (M1,f) is nonpositive & Integral1 (M1,(f | B)) is nonpositive & Integral2 (M2,f) is nonpositive & Integral2 (M2,(f | B)) is nonpositive ) )
assume that
A1:
A = dom f
and
A2:
f is nonpositive
and
A3:
f is A -measurable
; ( Integral1 (M1,f) is nonpositive & Integral1 (M1,(f | B)) is nonpositive & Integral2 (M2,f) is nonpositive & Integral2 (M2,(f | B)) is nonpositive )
A4:
f | B is nonpositive
by A2, MESFUN11:1;
A5:
dom (f | B) = A /\ B
by A1, RELAT_1:61;
A6:
f is A /\ B -measurable
by A3, XBOOLE_1:17, MESFUNC1:30;
A7:
(dom f) /\ (A /\ B) = A /\ B
by A1, XBOOLE_1:17, XBOOLE_1:28;
f | (A /\ B) = (f | A) /\ (f | B)
by RELAT_1:79;
then
f | (A /\ B) = f | B
by A1, RELAT_1:59, XBOOLE_1:28;
then A8:
f | B is A /\ B -measurable
by A6, A7, MESFUNC5:42;
now for y being set st y in dom (Integral1 (M1,f)) holds
(Integral1 (M1,f)) . y <= 0 let y be
set ;
( y in dom (Integral1 (M1,f)) implies (Integral1 (M1,f)) . y <= 0 )assume
y in dom (Integral1 (M1,f))
;
(Integral1 (M1,f)) . y <= 0 then reconsider y1 =
y as
Element of
X2 ;
A9:
ProjPMap2 (
f,
y1) is
Measurable-Y-section (
A,
y1)
-measurable
by A1, A3, Th47;
dom (ProjPMap2 (f,y1)) = Y-section (
A,
y1)
by A1, Def4;
then
dom (ProjPMap2 (f,y1)) = Measurable-Y-section (
A,
y1)
by MEASUR11:def 7;
then
Integral (
M1,
(ProjPMap2 (f,y1)))
<= 0
by A2, A9, Th33, MESFUN11:61;
hence
(Integral1 (M1,f)) . y <= 0
by Def7;
verum end;
hence
Integral1 (M1,f) is nonpositive
by MESFUNC5:9; ( Integral1 (M1,(f | B)) is nonpositive & Integral2 (M2,f) is nonpositive & Integral2 (M2,(f | B)) is nonpositive )
now for y being set st y in dom (Integral1 (M1,(f | B))) holds
(Integral1 (M1,(f | B))) . y <= 0 let y be
set ;
( y in dom (Integral1 (M1,(f | B))) implies (Integral1 (M1,(f | B))) . y <= 0 )assume
y in dom (Integral1 (M1,(f | B)))
;
(Integral1 (M1,(f | B))) . y <= 0 then reconsider y1 =
y as
Element of
X2 ;
A10:
ProjPMap2 (
(f | B),
y1) is
Measurable-Y-section (
(A /\ B),
y1)
-measurable
by A5, A8, Th47;
dom (ProjPMap2 ((f | B),y1)) = Y-section (
(A /\ B),
y1)
by A5, Def4;
then
dom (ProjPMap2 ((f | B),y1)) = Measurable-Y-section (
(A /\ B),
y1)
by MEASUR11:def 7;
then
Integral (
M1,
(ProjPMap2 ((f | B),y1)))
<= 0
by A4, A10, Th33, MESFUN11:61;
hence
(Integral1 (M1,(f | B))) . y <= 0
by Def7;
verum end;
hence
Integral1 (M1,(f | B)) is nonpositive
by MESFUNC5:9; ( Integral2 (M2,f) is nonpositive & Integral2 (M2,(f | B)) is nonpositive )
now for x being set st x in dom (Integral2 (M2,f)) holds
(Integral2 (M2,f)) . x <= 0 let x be
set ;
( x in dom (Integral2 (M2,f)) implies (Integral2 (M2,f)) . x <= 0 )assume
x in dom (Integral2 (M2,f))
;
(Integral2 (M2,f)) . x <= 0 then reconsider x1 =
x as
Element of
X1 ;
A9:
ProjPMap1 (
f,
x1) is
Measurable-X-section (
A,
x1)
-measurable
by A1, A3, Th47;
dom (ProjPMap1 (f,x1)) = X-section (
A,
x1)
by A1, Def3;
then
dom (ProjPMap1 (f,x1)) = Measurable-X-section (
A,
x1)
by MEASUR11:def 6;
then
Integral (
M2,
(ProjPMap1 (f,x1)))
<= 0
by A2, A9, Th33, MESFUN11:61;
hence
(Integral2 (M2,f)) . x <= 0
by Def8;
verum end;
hence
Integral2 (M2,f) is nonpositive
by MESFUNC5:9; Integral2 (M2,(f | B)) is nonpositive
now for x being set st x in dom (Integral2 (M2,(f | B))) holds
(Integral2 (M2,(f | B))) . x <= 0 let x be
set ;
( x in dom (Integral2 (M2,(f | B))) implies (Integral2 (M2,(f | B))) . x <= 0 )assume
x in dom (Integral2 (M2,(f | B)))
;
(Integral2 (M2,(f | B))) . x <= 0 then reconsider x1 =
x as
Element of
X1 ;
A10:
ProjPMap1 (
(f | B),
x1) is
Measurable-X-section (
(A /\ B),
x1)
-measurable
by A5, A8, Th47;
dom (ProjPMap1 ((f | B),x1)) = X-section (
(A /\ B),
x1)
by A5, Def3;
then
dom (ProjPMap1 ((f | B),x1)) = Measurable-X-section (
(A /\ B),
x1)
by MEASUR11:def 6;
then
Integral (
M2,
(ProjPMap1 ((f | B),x1)))
<= 0
by A4, A10, Th33, MESFUN11:61;
hence
(Integral2 (M2,(f | B))) . x <= 0
by Def8;
verum end;
hence
Integral2 (M2,(f | B)) is nonpositive
by MESFUNC5:9; verum