:: by Noboru Endou

::

:: Received March 27, 2018

:: Copyright (c) 2018 Association of Mizar Users

definition

let A, X be set ;

let er be ExtReal;

ex b_{1} being Function of X,ExtREAL st

for x being object st x in X holds

( ( x in A implies b_{1} . x = er ) & ( not x in A implies b_{1} . x = 0 ) )

for b_{1}, b_{2} being Function of X,ExtREAL st ( for x being object st x in X holds

( ( x in A implies b_{1} . x = er ) & ( not x in A implies b_{1} . x = 0 ) ) ) & ( for x being object st x in X holds

( ( x in A implies b_{2} . x = er ) & ( not x in A implies b_{2} . x = 0 ) ) ) holds

b_{1} = b_{2}

end;
let er be ExtReal;

func chi (er,A,X) -> Function of X,ExtREAL means :Def1: :: MESFUN12:def 1

for x being object st x in X holds

( ( x in A implies it . x = er ) & ( not x in A implies it . x = 0 ) );

existence for x being object st x in X holds

( ( x in A implies it . x = er ) & ( not x in A implies it . x = 0 ) );

ex b

for x being object st x in X holds

( ( x in A implies b

proof end;

uniqueness for b

( ( x in A implies b

( ( x in A implies b

b

proof end;

:: deftheorem Def1 defines chi MESFUN12:def 1 :

for A, X being set

for er being ExtReal

for b_{4} being Function of X,ExtREAL holds

( b_{4} = chi (er,A,X) iff for x being object st x in X holds

( ( x in A implies b_{4} . x = er ) & ( not x in A implies b_{4} . x = 0 ) ) );

for A, X being set

for er being ExtReal

for b

( b

( ( x in A implies b

theorem Th2: :: MESFUN12:2

for X being non empty set

for A being set holds

( chi (+infty,A,X) = Xchi (A,X) & chi (-infty,A,X) = - (Xchi (A,X)) )

for A being set holds

( chi (+infty,A,X) = Xchi (A,X) & chi (-infty,A,X) = - (Xchi (A,X)) )

proof end;

theorem Th4: :: MESFUN12:4

for X being non empty set

for A being set

for r being Real holds

( rng (chi (r,A,X)) c= {0,r} & chi (r,A,X) is V121() & chi (r,A,X) is V120() )

for A being set

for r being Real holds

( rng (chi (r,A,X)) c= {0,r} & chi (r,A,X) is V121() & chi (r,A,X) is V120() )

proof end;

theorem Th5: :: MESFUN12:5

for X being non empty set

for S being SigmaField of X

for f being non empty PartFunc of X,ExtREAL

for M being sigma_Measure of S st f is_simple_func_in S holds

ex E being non empty Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL ex r being FinSequence of REAL st

( E,a are_Re-presentation_of f & ( for n being Nat holds

( a . n = r . n & f | (E . n) = (chi ((r . n),(E . n),X)) | (E . n) & ( E . n = {} implies r . n = 0 ) ) ) )

for S being SigmaField of X

for f being non empty PartFunc of X,ExtREAL

for M being sigma_Measure of S st f is_simple_func_in S holds

ex E being non empty Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL ex r being FinSequence of REAL st

( E,a are_Re-presentation_of f & ( for n being Nat holds

( a . n = r . n & f | (E . n) = (chi ((r . n),(E . n),X)) | (E . n) & ( E . n = {} implies r . n = 0 ) ) ) )

proof end;

definition

let F be FinSequence-like Function;

( F is disjoint_valued iff for m, n being Nat st m in dom F & n in dom F & m <> n holds

F . m misses F . n )

end;
redefine attr F is disjoint_valued means :Def2: :: MESFUN12:def 2

for m, n being Nat st m in dom F & n in dom F & m <> n holds

F . m misses F . n;

compatibility for m, n being Nat st m in dom F & n in dom F & m <> n holds

F . m misses F . n;

( F is disjoint_valued iff for m, n being Nat st m in dom F & n in dom F & m <> n holds

F . m misses F . n )

proof end;

:: deftheorem Def2 defines disjoint_valued MESFUN12:def 2 :

for F being FinSequence-like Function holds

( F is disjoint_valued iff for m, n being Nat st m in dom F & n in dom F & m <> n holds

F . m misses F . n );

for F being FinSequence-like Function holds

( F is disjoint_valued iff for m, n being Nat st m in dom F & n in dom F & m <> n holds

F . m misses F . n );

theorem Th6: :: MESFUN12:6

for X being non empty set

for S being SigmaField of X

for E1, E2 being Element of S st E1 misses E2 holds

<*E1,E2*> is Finite_Sep_Sequence of S

for S being SigmaField of X

for E1, E2 being Element of S st E1 misses E2 holds

<*E1,E2*> is Finite_Sep_Sequence of S

proof end;

theorem Th7: :: MESFUN12:7

for X being non empty set

for A1, A2 being Subset of X

for r1, r2 being Real holds <*(chi (r1,A1,X)),(chi (r2,A2,X))*> is summable FinSequence of Funcs (X,ExtREAL)

for A1, A2 being Subset of X

for r1, r2 being Real holds <*(chi (r1,A1,X)),(chi (r2,A2,X))*> is summable FinSequence of Funcs (X,ExtREAL)

proof end;

theorem Th8: :: MESFUN12:8

for X being non empty set

for F being summable FinSequence of Funcs (X,ExtREAL) st len F >= 2 holds

(Partial_Sums F) /. 2 = (F /. 1) + (F /. 2)

for F being summable FinSequence of Funcs (X,ExtREAL) st len F >= 2 holds

(Partial_Sums F) /. 2 = (F /. 1) + (F /. 2)

proof end;

theorem Th10: :: MESFUN12:10

for X being non empty set

for F being summable FinSequence of Funcs (X,ExtREAL) holds

( dom F = dom (Partial_Sums F) & ( for n being Nat st n in dom F holds

(Partial_Sums F) /. n = (Partial_Sums F) . n ) & ( for n being Nat

for x being Element of X st 1 <= n & n < len F holds

((Partial_Sums F) /. (n + 1)) . x = (((Partial_Sums F) /. n) . x) + ((F /. (n + 1)) . x) ) )

for F being summable FinSequence of Funcs (X,ExtREAL) holds

( dom F = dom (Partial_Sums F) & ( for n being Nat st n in dom F holds

(Partial_Sums F) /. n = (Partial_Sums F) . n ) & ( for n being Nat

for x being Element of X st 1 <= n & n < len F holds

((Partial_Sums F) /. (n + 1)) . x = (((Partial_Sums F) /. n) . x) + ((F /. (n + 1)) . x) ) )

proof end;

theorem Th11: :: MESFUN12:11

for X being non empty set

for S being SigmaField of X

for f being Function of X,ExtREAL

for E being Finite_Sep_Sequence of S

for F being summable FinSequence of Funcs (X,ExtREAL) st dom E = dom F & dom f = union (rng E) & ( for n being Nat st n in dom F holds

ex r being Real st F /. n = r (#) (chi ((E . n),X)) ) & f = (Partial_Sums F) /. (len F) holds

( ( for x being Element of X

for m, n being Nat st m in dom F & n in dom F & x in E . m & m <> n holds

(F /. n) . x = 0 ) & ( for x being Element of X

for m, n being Nat st m in dom F & n in dom F & x in E . m & n < m holds

((Partial_Sums F) /. n) . x = 0 ) & ( for x being Element of X

for m, n being Nat st m in dom F & n in dom F & x in E . m & n >= m holds

((Partial_Sums F) /. n) . x = f . x ) & ( for x being Element of X

for m being Nat st m in dom F & x in E . m holds

(F /. m) . x = f . x ) & f is_simple_func_in S )

for S being SigmaField of X

for f being Function of X,ExtREAL

for E being Finite_Sep_Sequence of S

for F being summable FinSequence of Funcs (X,ExtREAL) st dom E = dom F & dom f = union (rng E) & ( for n being Nat st n in dom F holds

ex r being Real st F /. n = r (#) (chi ((E . n),X)) ) & f = (Partial_Sums F) /. (len F) holds

( ( for x being Element of X

for m, n being Nat st m in dom F & n in dom F & x in E . m & m <> n holds

(F /. n) . x = 0 ) & ( for x being Element of X

for m, n being Nat st m in dom F & n in dom F & x in E . m & n < m holds

((Partial_Sums F) /. n) . x = 0 ) & ( for x being Element of X

for m, n being Nat st m in dom F & n in dom F & x in E . m & n >= m holds

((Partial_Sums F) /. n) . x = f . x ) & ( for x being Element of X

for m being Nat st m in dom F & x in E . m holds

(F /. m) . x = f . x ) & f is_simple_func_in S )

proof end;

theorem Th12: :: MESFUN12:12

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S holds chi (E,X) is_simple_func_in S

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S holds chi (E,X) is_simple_func_in S

proof end;

theorem Th13: :: MESFUN12:13

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for A, B being Element of S

for er being ExtReal holds chi (er,A,X) is_measurable_on B

for S being SigmaField of X

for M being sigma_Measure of S

for A, B being Element of S

for er being ExtReal holds chi (er,A,X) is_measurable_on B

proof end;

theorem Th14: :: MESFUN12:14

for X being set

for A1, A2 being Subset of X

for er being ExtReal holds (chi (er,A1,X)) | A2 = (chi (er,(A1 /\ A2),X)) | A2

for A1, A2 being Subset of X

for er being ExtReal holds (chi (er,A1,X)) | A2 = (chi (er,(A1 /\ A2),X)) | A2

proof end;

theorem Th15: :: MESFUN12:15

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for A, B, C being Element of S

for er being ExtReal st C c= B holds

(chi (er,A,X)) | B is_measurable_on C

for S being SigmaField of X

for M being sigma_Measure of S

for A, B, C being Element of S

for er being ExtReal st C c= B holds

(chi (er,A,X)) | B is_measurable_on C

proof end;

theorem Th16: :: MESFUN12:16

for X being set

for A1, A2 being Subset of X

for er being ExtReal

for x being object st A1 misses A2 holds

((chi (er,A1,X)) | A2) . x = 0

for A1, A2 being Subset of X

for er being ExtReal

for x being object st A1 misses A2 holds

((chi (er,A1,X)) | A2) . x = 0

proof end;

theorem Th17: :: MESFUN12:17

for X being set

for A being Subset of X

for er being ExtReal holds

( ( er >= 0 implies chi (er,A,X) is nonnegative ) & ( er <= 0 implies chi (er,A,X) is nonpositive ) )

for A being Subset of X

for er being ExtReal holds

( ( er >= 0 implies chi (er,A,X) is nonnegative ) & ( er <= 0 implies chi (er,A,X) is nonpositive ) )

proof end;

theorem Th19: :: MESFUN12:19

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL st f is empty holds

f is_simple_func_in S

for S being SigmaField of X

for f being PartFunc of X,ExtREAL st f is empty holds

f is_simple_func_in S

proof end;

theorem Th20: :: MESFUN12:20

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E1, E2 being Element of S holds Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)

for S being SigmaField of X

for M being sigma_Measure of S

for E1, E2 being Element of S holds Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)

proof end;

theorem Th21: :: MESFUN12:21

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E1, E2 being Element of S

for f, g being PartFunc of X,ExtREAL st E1 = dom f & f is nonnegative & f is_measurable_on E1 & E2 = dom g & g is nonnegative & g is_measurable_on E2 holds

Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g)))))

for S being SigmaField of X

for M being sigma_Measure of S

for E1, E2 being Element of S

for f, g being PartFunc of X,ExtREAL st E1 = dom f & f is nonnegative & f is_measurable_on E1 & E2 = dom g & g is nonnegative & g is_measurable_on E2 holds

Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g)))))

proof end;

theorem Th22: :: MESFUN12:22

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E1, E2 being Element of S

for f, g being PartFunc of X,ExtREAL st E1 = dom f & f is nonpositive & f is_measurable_on E1 & E2 = dom g & g is nonpositive & g is_measurable_on E2 holds

Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g)))))

for S being SigmaField of X

for M being sigma_Measure of S

for E1, E2 being Element of S

for f, g being PartFunc of X,ExtREAL st E1 = dom f & f is nonpositive & f is_measurable_on E1 & E2 = dom g & g is nonpositive & g is_measurable_on E2 holds

Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g)))))

proof end;

theorem :: MESFUN12:23

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E1, E2 being Element of S

for f, g being PartFunc of X,ExtREAL st E1 = dom f & f is nonnegative & f is_measurable_on E1 & E2 = dom g & g is nonpositive & g is_measurable_on E2 holds

( Integral (M,(f - g)) = (Integral (M,(f | (dom (f - g))))) - (Integral (M,(g | (dom (f - g))))) & Integral (M,(g - f)) = (Integral (M,(g | (dom (g - f))))) - (Integral (M,(f | (dom (g - f))))) )

for S being SigmaField of X

for M being sigma_Measure of S

for E1, E2 being Element of S

for f, g being PartFunc of X,ExtREAL st E1 = dom f & f is nonnegative & f is_measurable_on E1 & E2 = dom g & g is nonpositive & g is_measurable_on E2 holds

( Integral (M,(f - g)) = (Integral (M,(f | (dom (f - g))))) - (Integral (M,(g | (dom (f - g))))) & Integral (M,(g - f)) = (Integral (M,(g | (dom (g - f))))) - (Integral (M,(f | (dom (g - f))))) )

proof end;

Lm1: for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,ExtREAL

for r being Real st E = dom f & f is nonnegative & f is_measurable_on E holds

Integral (M,(r (#) f)) = r * (Integral (M,f))

proof end;

Lm2: for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,ExtREAL

for r being Real st E = dom f & f is nonpositive & f is_measurable_on E holds

Integral (M,(r (#) f)) = r * (Integral (M,f))

proof end;

theorem :: MESFUN12:24

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,ExtREAL

for r being Real st E = dom f & ( f is nonpositive or f is nonnegative ) & f is_measurable_on E holds

Integral (M,(r (#) f)) = r * (Integral (M,f)) by Lm1, Lm2;

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,ExtREAL

for r being Real st E = dom f & ( f is nonpositive or f is nonnegative ) & f is_measurable_on E holds

Integral (M,(r (#) f)) = r * (Integral (M,f)) by Lm1, Lm2;

theorem Th25: :: MESFUN12:25

for X, Y being non empty set

for A being Element of bool [:X,Y:]

for x, y being set st x in X & y in Y holds

( ( [x,y] in A implies x in Y-section (A,y) ) & ( x in Y-section (A,y) implies [x,y] in A ) & ( [x,y] in A implies y in X-section (A,x) ) & ( y in X-section (A,x) implies [x,y] in A ) )

for A being Element of bool [:X,Y:]

for x, y being set st x in X & y in Y holds

( ( [x,y] in A implies x in Y-section (A,y) ) & ( x in Y-section (A,y) implies [x,y] in A ) & ( [x,y] in A implies y in X-section (A,x) ) & ( y in X-section (A,x) implies [x,y] in A ) )

proof end;

definition

let X1, X2 be non empty set ;

let Y be set ;

let f be PartFunc of [:X1,X2:],Y;

let x be Element of X1;

ex b_{1} being PartFunc of X2,Y st

( dom b_{1} = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds

b_{1} . y = f . (x,y) ) )

for b_{1}, b_{2} being PartFunc of X2,Y st dom b_{1} = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds

b_{1} . y = f . (x,y) ) & dom b_{2} = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds

b_{2} . y = f . (x,y) ) holds

b_{1} = b_{2}

end;
let Y be set ;

let f be PartFunc of [:X1,X2:],Y;

let x be Element of X1;

func ProjPMap1 (f,x) -> PartFunc of X2,Y means :Def3: :: MESFUN12:def 3

( dom it = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds

it . y = f . (x,y) ) );

existence ( dom it = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds

it . y = f . (x,y) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines ProjPMap1 MESFUN12:def 3 :

for X1, X2 being non empty set

for Y being set

for f being PartFunc of [:X1,X2:],Y

for x being Element of X1

for b_{6} being PartFunc of X2,Y holds

( b_{6} = ProjPMap1 (f,x) iff ( dom b_{6} = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds

b_{6} . y = f . (x,y) ) ) );

for X1, X2 being non empty set

for Y being set

for f being PartFunc of [:X1,X2:],Y

for x being Element of X1

for b

( b

b

definition

let X1, X2 be non empty set ;

let Y be set ;

let f be PartFunc of [:X1,X2:],Y;

let y be Element of X2;

ex b_{1} being PartFunc of X1,Y st

( dom b_{1} = Y-section ((dom f),y) & ( for x being Element of X1 st [x,y] in dom f holds

b_{1} . x = f . (x,y) ) )

for b_{1}, b_{2} being PartFunc of X1,Y st dom b_{1} = Y-section ((dom f),y) & ( for x being Element of X1 st [x,y] in dom f holds

b_{1} . x = f . (x,y) ) & dom b_{2} = Y-section ((dom f),y) & ( for x being Element of X1 st [x,y] in dom f holds

b_{2} . x = f . (x,y) ) holds

b_{1} = b_{2}

end;
let Y be set ;

let f be PartFunc of [:X1,X2:],Y;

let y be Element of X2;

func ProjPMap2 (f,y) -> PartFunc of X1,Y means :Def4: :: MESFUN12:def 4

( dom it = Y-section ((dom f),y) & ( for x being Element of X1 st [x,y] in dom f holds

it . x = f . (x,y) ) );

existence ( dom it = Y-section ((dom f),y) & ( for x being Element of X1 st [x,y] in dom f holds

it . x = f . (x,y) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines ProjPMap2 MESFUN12:def 4 :

for X1, X2 being non empty set

for Y being set

for f being PartFunc of [:X1,X2:],Y

for y being Element of X2

for b_{6} being PartFunc of X1,Y holds

( b_{6} = ProjPMap2 (f,y) iff ( dom b_{6} = Y-section ((dom f),y) & ( for x being Element of X1 st [x,y] in dom f holds

b_{6} . x = f . (x,y) ) ) );

for X1, X2 being non empty set

for Y being set

for f being PartFunc of [:X1,X2:],Y

for y being Element of X2

for b

( b

b

theorem Th26: :: MESFUN12:26

for X1, X2 being non empty set

for Y being set

for f being PartFunc of [:X1,X2:],Y

for x being Element of X1

for y being Element of X2 holds

( ( x in dom (ProjPMap2 (f,y)) implies (ProjPMap2 (f,y)) . x = f . (x,y) ) & ( y in dom (ProjPMap1 (f,x)) implies (ProjPMap1 (f,x)) . y = f . (x,y) ) )

for Y being set

for f being PartFunc of [:X1,X2:],Y

for x being Element of X1

for y being Element of X2 holds

( ( x in dom (ProjPMap2 (f,y)) implies (ProjPMap2 (f,y)) . x = f . (x,y) ) & ( y in dom (ProjPMap1 (f,x)) implies (ProjPMap1 (f,x)) . y = f . (x,y) ) )

proof end;

theorem Th27: :: MESFUN12:27

for X1, X2, Y being non empty set

for f being Function of [:X1,X2:],Y

for x being Element of X1

for y being Element of X2 holds

( ProjPMap1 (f,x) = ProjMap1 (f,x) & ProjPMap2 (f,y) = ProjMap2 (f,y) )

for f being Function of [:X1,X2:],Y

for x being Element of X1

for y being Element of X2 holds

( ProjPMap1 (f,x) = ProjMap1 (f,x) & ProjPMap2 (f,y) = ProjMap2 (f,y) )

proof end;

theorem :: MESFUN12:28

for X, Y, Z being non empty set

for f being PartFunc of [:X,Y:],Z

for x being Element of X

for y being Element of Y

for A being set holds

( X-section ((f " A),x) = (ProjPMap1 (f,x)) " A & Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A )

for f being PartFunc of [:X,Y:],Z

for x being Element of X

for y being Element of Y

for A being set holds

( X-section ((f " A),x) = (ProjPMap1 (f,x)) " A & Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A )

proof end;

theorem Th29: :: MESFUN12:29

for X1, X2 being non empty set

for x being Element of X1

for y being Element of X2

for r being Real

for f being PartFunc of [:X1,X2:],ExtREAL holds

( ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x)) & ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y)) )

for x being Element of X1

for y being Element of X2

for r being Real

for f being PartFunc of [:X1,X2:],ExtREAL holds

( ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x)) & ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y)) )

proof end;

theorem :: MESFUN12:30

for X1, X2 being non empty set

for f being PartFunc of [:X1,X2:],ExtREAL

for x being Element of X1

for y being Element of X2 st ( for z being Element of [:X1,X2:] st z in dom f holds

f . z = 0 ) holds

( (ProjPMap2 (f,y)) . x = 0 & (ProjPMap1 (f,x)) . y = 0 )

for f being PartFunc of [:X1,X2:],ExtREAL

for x being Element of X1

for y being Element of X2 st ( for z being Element of [:X1,X2:] st z in dom f holds

f . z = 0 ) holds

( (ProjPMap2 (f,y)) . x = 0 & (ProjPMap1 (f,x)) . y = 0 )

proof end;

theorem Th31: :: MESFUN12:31

for X1, X2 being non empty set

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 )

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 )

proof end;

theorem Th32: :: MESFUN12:32

for X1, X2 being non empty set

for x being Element of X1

for y being Element of X2

for f being PartFunc of [:X1,X2:],ExtREAL st f is nonnegative holds

( ProjPMap1 (f,x) is nonnegative & ProjPMap2 (f,y) is nonnegative )

for x being Element of X1

for y being Element of X2

for f being PartFunc of [:X1,X2:],ExtREAL st f is nonnegative holds

( ProjPMap1 (f,x) is nonnegative & ProjPMap2 (f,y) is nonnegative )

proof end;

theorem Th33: :: MESFUN12:33

for X1, X2 being non empty set

for x being Element of X1

for y being Element of X2

for f being PartFunc of [:X1,X2:],ExtREAL st f is nonpositive holds

( ProjPMap1 (f,x) is nonpositive & ProjPMap2 (f,y) is nonpositive )

for x being Element of X1

for y being Element of X2

for f being PartFunc of [:X1,X2:],ExtREAL st f is nonpositive holds

( ProjPMap1 (f,x) is nonpositive & ProjPMap2 (f,y) is nonpositive )

proof end;

theorem Th34: :: MESFUN12:34

for X1, X2 being non empty set

for x being Element of X1

for y being Element of X2

for A being Subset of [:X1,X2:]

for f being PartFunc of [:X1,X2:],ExtREAL holds

( ProjPMap1 ((f | A),x) = (ProjPMap1 (f,x)) | (X-section (A,x)) & ProjPMap2 ((f | A),y) = (ProjPMap2 (f,y)) | (Y-section (A,y)) )

for x being Element of X1

for y being Element of X2

for A being Subset of [:X1,X2:]

for f being PartFunc of [:X1,X2:],ExtREAL holds

( ProjPMap1 ((f | A),x) = (ProjPMap1 (f,x)) | (X-section (A,x)) & ProjPMap2 ((f | A),y) = (ProjPMap2 (f,y)) | (Y-section (A,y)) )

proof end;

theorem Th35: :: MESFUN12:35

for X1, X2 being non empty set

for A being Subset of [:X1,X2:]

for x being Element of X1

for y being Element of X2 holds

( ProjPMap1 ((Xchi (A,[:X1,X2:])),x) = Xchi ((X-section (A,x)),X2) & ProjPMap2 ((Xchi (A,[:X1,X2:])),y) = Xchi ((Y-section (A,y)),X1) )

for A being Subset of [:X1,X2:]

for x being Element of X1

for y being Element of X2 holds

( ProjPMap1 ((Xchi (A,[:X1,X2:])),x) = Xchi ((X-section (A,x)),X2) & ProjPMap2 ((Xchi (A,[:X1,X2:])),y) = Xchi ((Y-section (A,y)),X1) )

proof end;

theorem Th36: :: MESFUN12:36

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL

for E being Element of S st f | E = g | E & E c= dom f & E c= dom g & f is_measurable_on E holds

g is_measurable_on E

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL

for E being Element of S st f | E = g | E & E c= dom f & E c= dom g & f is_measurable_on E holds

g is_measurable_on E

proof end;

theorem Th37: :: MESFUN12:37

for X1, X2 being non empty set

for A being Subset of [:X1,X2:]

for f being PartFunc of [:X1,X2:],ExtREAL

for x being Element of X1

for y being Element of X2

for F being Functional_Sequence of [:X1,X2:],ExtREAL st A c= dom f & ( for n being Nat holds dom (F . n) = A ) & ( for z being Element of [:X1,X2:] st z in A holds

( F # z is convergent & lim (F # z) = f . z ) ) holds

( ex FX being with_the_same_dom Functional_Sequence of X1,ExtREAL st

( ( for n being Nat holds FX . n = ProjPMap2 ((F . n),y) ) & ( for x being Element of X1 st x in Y-section (A,y) holds

( FX # x is convergent & (ProjPMap2 (f,y)) . x = lim (FX # x) ) ) ) & ex FY being with_the_same_dom Functional_Sequence of X2,ExtREAL st

( ( for n being Nat holds FY . n = ProjPMap1 ((F . n),x) ) & ( for y being Element of X2 st y in X-section (A,x) holds

( FY # y is convergent & (ProjPMap1 (f,x)) . y = lim (FY # y) ) ) ) )

for A being Subset of [:X1,X2:]

for f being PartFunc of [:X1,X2:],ExtREAL

for x being Element of X1

for y being Element of X2

for F being Functional_Sequence of [:X1,X2:],ExtREAL st A c= dom f & ( for n being Nat holds dom (F . n) = A ) & ( for z being Element of [:X1,X2:] st z in A holds

( F # z is convergent & lim (F # z) = f . z ) ) holds

( ex FX being with_the_same_dom Functional_Sequence of X1,ExtREAL st

( ( for n being Nat holds FX . n = ProjPMap2 ((F . n),y) ) & ( for x being Element of X1 st x in Y-section (A,y) holds

( FX # x is convergent & (ProjPMap2 (f,y)) . x = lim (FX # x) ) ) ) & ex FY being with_the_same_dom Functional_Sequence of X2,ExtREAL st

( ( for n being Nat holds FY . n = ProjPMap1 ((F . n),x) ) & ( for y being Element of X2 st y in X-section (A,x) holds

( FY # y is convergent & (ProjPMap1 (f,x)) . y = lim (FY # y) ) ) ) )

proof end;

Lm3: for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for f being PartFunc of [:X1,X2:],ExtREAL

for x being Element of X1

for y being Element of X2

for A being Element of sigma (measurable_rectangles (S1,S2)) st ( f is nonnegative or f is nonpositive ) & A c= dom f & f is_measurable_on A holds

( ProjPMap1 (f,x) is_measurable_on Measurable-X-section (A,x) & ProjPMap2 (f,y) is_measurable_on Measurable-Y-section (A,y) )

proof end;

theorem :: MESFUN12:38

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for E being Element of sigma (measurable_rectangles (S1,S2))

for M2 being sigma_Measure of S2

for A being Element of S1

for B being Element of S2

for x being Element of X1 holds (M2 . (B /\ (Measurable-X-section (E,x)))) * ((chi (A,X1)) . x) = Integral (M2,(ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)))

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for E being Element of sigma (measurable_rectangles (S1,S2))

for M2 being sigma_Measure of S2

for A being Element of S1

for B being Element of S2

for x being Element of X1 holds (M2 . (B /\ (Measurable-X-section (E,x)))) * ((chi (A,X1)) . x) = Integral (M2,(ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)))

proof end;

theorem :: MESFUN12:39

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for E being Element of sigma (measurable_rectangles (S1,S2))

for M1 being sigma_Measure of S1

for A being Element of S1

for B being Element of S2

for y being Element of X2 holds (M1 . (A /\ (Measurable-Y-section (E,y)))) * ((chi (B,X2)) . y) = Integral (M1,(ProjPMap2 (((chi ([:A,B:],[:X1,X2:])) | E),y)))

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for E being Element of sigma (measurable_rectangles (S1,S2))

for M1 being sigma_Measure of S1

for A being Element of S1

for B being Element of S2

for y being Element of X2 holds (M1 . (A /\ (Measurable-Y-section (E,y)))) * ((chi (B,X2)) . y) = Integral (M1,(ProjPMap2 (((chi ([:A,B:],[:X1,X2:])) | E),y)))

proof end;

theorem Th40: :: MESFUN12:40

for X1, X2 being non empty set

for x being Element of X1

for y being Element of X2

for f being PartFunc of [:X1,X2:],ExtREAL

for er being ExtReal holds

( ( [x,y] in dom f & f . (x,y) = er implies ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = er ) ) & ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = er implies ( [x,y] in dom f & f . (x,y) = er ) ) & ( [x,y] in dom f & f . (x,y) = er implies ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = er ) ) & ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = er implies ( [x,y] in dom f & f . (x,y) = er ) ) )

for x being Element of X1

for y being Element of X2

for f being PartFunc of [:X1,X2:],ExtREAL

for er being ExtReal holds

( ( [x,y] in dom f & f . (x,y) = er implies ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = er ) ) & ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = er implies ( [x,y] in dom f & f . (x,y) = er ) ) & ( [x,y] in dom f & f . (x,y) = er implies ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = er ) ) & ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = er implies ( [x,y] in dom f & f . (x,y) = er ) ) )

proof end;

theorem Th41: :: MESFUN12:41

for X1, X2 being non empty set

for A, Z being set

for f being PartFunc of [:X1,X2:],Z

for x being Element of X1 holds X-section ((f " A),x) = (ProjPMap1 (f,x)) " A

for A, Z being set

for f being PartFunc of [:X1,X2:],Z

for x being Element of X1 holds X-section ((f " A),x) = (ProjPMap1 (f,x)) " A

proof end;

theorem Th42: :: MESFUN12:42

for X1, X2 being non empty set

for A, Z being set

for f being PartFunc of [:X1,X2:],Z

for y being Element of X2 holds Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A

for A, Z being set

for f being PartFunc of [:X1,X2:],Z

for y being Element of X2 holds Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A

proof end;

theorem Th43: :: MESFUN12:43

for X1, X2 being non empty set

for A, B being Subset of [:X1,X2:]

for p being set holds

( X-section ((A \ B),p) = (X-section (A,p)) \ (X-section (B,p)) & Y-section ((A \ B),p) = (Y-section (A,p)) \ (Y-section (B,p)) )

for A, B being Subset of [:X1,X2:]

for p being set holds

( X-section ((A \ B),p) = (X-section (A,p)) \ (X-section (B,p)) & Y-section ((A \ B),p) = (Y-section (A,p)) \ (Y-section (B,p)) )

proof end;

theorem Th44: :: MESFUN12:44

for X1, X2 being non empty set

for x being Element of X1

for y being Element of X2

for f1, f2 being PartFunc of [:X1,X2:],ExtREAL holds

( ProjPMap1 ((f1 + f2),x) = (ProjPMap1 (f1,x)) + (ProjPMap1 (f2,x)) & ProjPMap1 ((f1 - f2),x) = (ProjPMap1 (f1,x)) - (ProjPMap1 (f2,x)) & ProjPMap2 ((f1 + f2),y) = (ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y)) & ProjPMap2 ((f1 - f2),y) = (ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y)) )

for x being Element of X1

for y being Element of X2

for f1, f2 being PartFunc of [:X1,X2:],ExtREAL holds

( ProjPMap1 ((f1 + f2),x) = (ProjPMap1 (f1,x)) + (ProjPMap1 (f2,x)) & ProjPMap1 ((f1 - f2),x) = (ProjPMap1 (f1,x)) - (ProjPMap1 (f2,x)) & ProjPMap2 ((f1 + f2),y) = (ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y)) & ProjPMap2 ((f1 - f2),y) = (ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y)) )

proof end;

Lm4: for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for f being PartFunc of [:X1,X2:],ExtREAL

for x being Element of X1

for y being Element of X2

for E being Element of sigma (measurable_rectangles (S1,S2)) st E c= dom f & f is_measurable_on E holds

( ProjPMap1 ((max+ f),x) is_measurable_on Measurable-X-section (E,x) & ProjPMap2 ((max+ f),y) is_measurable_on Measurable-Y-section (E,y) & ProjPMap1 ((max- f),x) is_measurable_on Measurable-X-section (E,x) & ProjPMap2 ((max- f),y) is_measurable_on Measurable-Y-section (E,y) )

proof end;

theorem Th45: :: MESFUN12:45

for X1, X2 being non empty set

for f being PartFunc of [:X1,X2:],ExtREAL

for x being Element of X1 holds

( ProjPMap1 ((max+ f),x) = max+ (ProjPMap1 (f,x)) & ProjPMap1 ((max- f),x) = max- (ProjPMap1 (f,x)) )

for f being PartFunc of [:X1,X2:],ExtREAL

for x being Element of X1 holds

( ProjPMap1 ((max+ f),x) = max+ (ProjPMap1 (f,x)) & ProjPMap1 ((max- f),x) = max- (ProjPMap1 (f,x)) )

proof end;

theorem Th46: :: MESFUN12:46

for X1, X2 being non empty set

for f being PartFunc of [:X1,X2:],ExtREAL

for y being Element of X2 holds

( ProjPMap2 ((max+ f),y) = max+ (ProjPMap2 (f,y)) & ProjPMap2 ((max- f),y) = max- (ProjPMap2 (f,y)) )

for f being PartFunc of [:X1,X2:],ExtREAL

for y being Element of X2 holds

( ProjPMap2 ((max+ f),y) = max+ (ProjPMap2 (f,y)) & ProjPMap2 ((max- f),y) = max- (ProjPMap2 (f,y)) )

proof end;

theorem Th47: :: MESFUN12:47

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for f being PartFunc of [:X1,X2:],ExtREAL

for x being Element of X1

for y being Element of X2

for E being Element of sigma (measurable_rectangles (S1,S2)) st E c= dom f & f is_measurable_on E holds

( ProjPMap1 (f,x) is_measurable_on Measurable-X-section (E,x) & ProjPMap2 (f,y) is_measurable_on Measurable-Y-section (E,y) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for f being PartFunc of [:X1,X2:],ExtREAL

for x being Element of X1

for y being Element of X2

for E being Element of sigma (measurable_rectangles (S1,S2)) st E c= dom f & f is_measurable_on E holds

( ProjPMap1 (f,x) is_measurable_on Measurable-X-section (E,x) & ProjPMap2 (f,y) is_measurable_on Measurable-Y-section (E,y) )

proof end;

definition

let X1, X2, Y be non empty set ;

let F be Functional_Sequence of [:X1,X2:],Y;

let x be Element of X1;

ex b_{1} being Functional_Sequence of X2,Y st

for n being Nat holds b_{1} . n = ProjPMap1 ((F . n),x)

for b_{1}, b_{2} being Functional_Sequence of X2,Y st ( for n being Nat holds b_{1} . n = ProjPMap1 ((F . n),x) ) & ( for n being Nat holds b_{2} . n = ProjPMap1 ((F . n),x) ) holds

b_{1} = b_{2}

end;
let F be Functional_Sequence of [:X1,X2:],Y;

let x be Element of X1;

func ProjPMap1 (F,x) -> Functional_Sequence of X2,Y means :Def5: :: MESFUN12:def 5

for n being Nat holds it . n = ProjPMap1 ((F . n),x);

existence for n being Nat holds it . n = ProjPMap1 ((F . n),x);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines ProjPMap1 MESFUN12:def 5 :

for X1, X2, Y being non empty set

for F being Functional_Sequence of [:X1,X2:],Y

for x being Element of X1

for b_{6} being Functional_Sequence of X2,Y holds

( b_{6} = ProjPMap1 (F,x) iff for n being Nat holds b_{6} . n = ProjPMap1 ((F . n),x) );

for X1, X2, Y being non empty set

for F being Functional_Sequence of [:X1,X2:],Y

for x being Element of X1

for b

( b

definition

let X1, X2, Y be non empty set ;

let F be Functional_Sequence of [:X1,X2:],Y;

let y be Element of X2;

ex b_{1} being Functional_Sequence of X1,Y st

for n being Nat holds b_{1} . n = ProjPMap2 ((F . n),y)

for b_{1}, b_{2} being Functional_Sequence of X1,Y st ( for n being Nat holds b_{1} . n = ProjPMap2 ((F . n),y) ) & ( for n being Nat holds b_{2} . n = ProjPMap2 ((F . n),y) ) holds

b_{1} = b_{2}

end;
let F be Functional_Sequence of [:X1,X2:],Y;

let y be Element of X2;

func ProjPMap2 (F,y) -> Functional_Sequence of X1,Y means :Def6: :: MESFUN12:def 6

for n being Nat holds it . n = ProjPMap2 ((F . n),y);

existence for n being Nat holds it . n = ProjPMap2 ((F . n),y);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines ProjPMap2 MESFUN12:def 6 :

for X1, X2, Y being non empty set

for F being Functional_Sequence of [:X1,X2:],Y

for y being Element of X2

for b_{6} being Functional_Sequence of X1,Y holds

( b_{6} = ProjPMap2 (F,y) iff for n being Nat holds b_{6} . n = ProjPMap2 ((F . n),y) );

for X1, X2, Y being non empty set

for F being Functional_Sequence of [:X1,X2:],Y

for y being Element of X2

for b

( b

theorem Th48: :: MESFUN12:48

for X1, X2 being non empty set

for E being Subset of [:X1,X2:]

for x being Element of X1

for y being Element of X2 holds

( ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((X-section (E,x)),X2) & ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Y-section (E,y)),X1) )

for E being Subset of [:X1,X2:]

for x being Element of X1

for y being Element of X2 holds

( ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((X-section (E,x)),X2) & ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Y-section (E,y)),X1) )

proof end;

theorem Th49: :: MESFUN12:49

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for er being ExtReal holds Integral (M,(chi (er,E,X))) = er * (M . E)

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for er being ExtReal holds Integral (M,(chi (er,E,X))) = er * (M . E)

proof end;

theorem Th50: :: MESFUN12:50

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for er being ExtReal holds Integral (M,((chi (er,E,X)) | E)) = er * (M . E)

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for er being ExtReal holds Integral (M,((chi (er,E,X)) | E)) = er * (M . E)

proof end;

theorem :: MESFUN12:51

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E1, E2 being Element of S

for er being ExtReal holds Integral (M,((chi (er,E1,X)) | E2)) = er * (M . (E1 /\ E2))

for S being SigmaField of X

for M being sigma_Measure of S

for E1, E2 being Element of S

for er being ExtReal holds Integral (M,((chi (er,E1,X)) | E2)) = er * (M . (E1 /\ E2))

proof end;

theorem Th52: :: MESFUN12:52

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for x being Element of X1

for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds

( (Y-vol (E,M2)) . x = Integral (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral+ (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral' (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for x being Element of X1

for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds

( (Y-vol (E,M2)) . x = Integral (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral+ (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral' (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) )

proof end;

theorem Th53: :: MESFUN12:53

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for y being Element of X2

for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds

( (X-vol (E,M1)) . y = Integral (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral+ (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral' (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for y being Element of X2

for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds

( (X-vol (E,M1)) . y = Integral (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral+ (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral' (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) )

proof end;

theorem :: MESFUN12:54

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for r being Real holds Integral (M,(r (#) (chi (E,X)))) = r * (Integral (M,(chi (E,X))))

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for r being Real holds Integral (M,(r (#) (chi (E,X)))) = r * (Integral (M,(chi (E,X))))

proof end;

theorem Th55: :: MESFUN12:55

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for y being Element of X2

for E being Element of sigma (measurable_rectangles (S1,S2))

for r being Real st M1 is sigma_finite holds

( (r (#) (X-vol (E,M1))) . y = Integral (M1,(ProjPMap2 ((chi (r,E,[:X1,X2:])),y))) & ( r >= 0 implies (r (#) (X-vol (E,M1))) . y = integral+ (M1,(ProjPMap2 ((chi (r,E,[:X1,X2:])),y))) ) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for y being Element of X2

for E being Element of sigma (measurable_rectangles (S1,S2))

for r being Real st M1 is sigma_finite holds

( (r (#) (X-vol (E,M1))) . y = Integral (M1,(ProjPMap2 ((chi (r,E,[:X1,X2:])),y))) & ( r >= 0 implies (r (#) (X-vol (E,M1))) . y = integral+ (M1,(ProjPMap2 ((chi (r,E,[:X1,X2:])),y))) ) )

proof end;

theorem Th56: :: MESFUN12:56

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for x being Element of X1

for E being Element of sigma (measurable_rectangles (S1,S2))

for r being Real st M2 is sigma_finite holds

( (r (#) (Y-vol (E,M2))) . x = Integral (M2,(ProjPMap1 ((chi (r,E,[:X1,X2:])),x))) & ( r >= 0 implies (r (#) (Y-vol (E,M2))) . x = integral+ (M2,(ProjPMap1 ((chi (r,E,[:X1,X2:])),x))) ) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for x being Element of X1

for E being Element of sigma (measurable_rectangles (S1,S2))

for r being Real st M2 is sigma_finite holds

( (r (#) (Y-vol (E,M2))) . x = Integral (M2,(ProjPMap1 ((chi (r,E,[:X1,X2:])),x))) & ( r >= 0 implies (r (#) (Y-vol (E,M2))) . x = integral+ (M2,(ProjPMap1 ((chi (r,E,[:X1,X2:])),x))) ) )

proof end;

theorem Th57: :: MESFUN12:57

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st dom f in S & ( for x being Element of X st x in dom f holds

0 = f . x ) holds

( ( for E being Element of S st E c= dom f holds

f is_measurable_on E ) & Integral (M,f) = 0 )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st dom f in S & ( for x being Element of X st x in dom f holds

0 = f . x ) holds

( ( for E being Element of S st E c= dom f holds

f is_measurable_on E ) & Integral (M,f) = 0 )

proof end;

Lm5: for X1, X2 being 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 A being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & ( f is nonnegative or f is nonpositive ) & A = dom f & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) holds

ex I1 being Function of X2,ExtREAL st

( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for V being Element of S2 holds I1 is_measurable_on V ) )

proof end;

Lm6: for X1, X2 being 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 A being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st M2 is sigma_finite & ( f is nonnegative or f is nonpositive ) & A = dom f & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) holds

ex I2 being Function of X1,ExtREAL st

( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is_measurable_on V ) )

proof end;

theorem Th58: :: MESFUN12:58

for X1, X2, Y being non empty set

for F being Functional_Sequence of [:X1,X2:],Y

for x being Element of X1

for y being Element of X2 st F is with_the_same_dom holds

( ProjPMap1 (F,x) is with_the_same_dom & ProjPMap2 (F,y) is with_the_same_dom )

for F being Functional_Sequence of [:X1,X2:],Y

for x being Element of X1

for y being Element of X2 st F is with_the_same_dom holds

( ProjPMap1 (F,x) is with_the_same_dom & ProjPMap2 (F,y) is with_the_same_dom )

proof end;

Lm7: for X1, X2 being 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 A being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & f is nonnegative & A = dom f & f is_measurable_on A holds

ex I1 being Function of X2,ExtREAL st

( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for V being Element of S2 holds I1 is_measurable_on V ) )

proof end;

Lm8: for X1, X2 being 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 A being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & f is nonpositive & A = dom f & f is_measurable_on A holds

ex I1 being Function of X2,ExtREAL st

( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for V being Element of S2 holds I1 is_measurable_on V ) )

proof end;

Lm9: for X1, X2 being 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 A being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st M2 is sigma_finite & f is nonnegative & A = dom f & f is_measurable_on A holds

ex I2 being Function of X1,ExtREAL st

( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is_measurable_on V ) )

proof end;

Lm10: for X1, X2 being 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 A being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st M2 is sigma_finite & f is nonpositive & A = dom f & f is_measurable_on A holds

ex I2 being Function of X1,ExtREAL st

( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is_measurable_on V ) )

proof end;

definition

let X1, X2 be non empty set ;

let S1 be SigmaField of X1;

let M1 be sigma_Measure of S1;

let f be PartFunc of [:X1,X2:],ExtREAL;

ex b_{1} being Function of X2,ExtREAL st

for y being Element of X2 holds b_{1} . y = Integral (M1,(ProjPMap2 (f,y)))

for b_{1}, b_{2} being Function of X2,ExtREAL st ( for y being Element of X2 holds b_{1} . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for y being Element of X2 holds b_{2} . y = Integral (M1,(ProjPMap2 (f,y))) ) holds

b_{1} = b_{2}

end;
let S1 be SigmaField of X1;

let M1 be sigma_Measure of S1;

let f be PartFunc of [:X1,X2:],ExtREAL;

func Integral1 (M1,f) -> Function of X2,ExtREAL means :Def7: :: MESFUN12:def 7

for y being Element of X2 holds it . y = Integral (M1,(ProjPMap2 (f,y)));

existence for y being Element of X2 holds it . y = Integral (M1,(ProjPMap2 (f,y)));

ex b

for y being Element of X2 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines Integral1 MESFUN12:def 7 :

for X1, X2 being non empty set

for S1 being SigmaField of X1

for M1 being sigma_Measure of S1

for f being PartFunc of [:X1,X2:],ExtREAL

for b_{6} being Function of X2,ExtREAL holds

( b_{6} = Integral1 (M1,f) iff for y being Element of X2 holds b_{6} . y = Integral (M1,(ProjPMap2 (f,y))) );

for X1, X2 being non empty set

for S1 being SigmaField of X1

for M1 being sigma_Measure of S1

for f being PartFunc of [:X1,X2:],ExtREAL

for b

( b

definition

let X1, X2 be non empty set ;

let S2 be SigmaField of X2;

let M2 be sigma_Measure of S2;

let f be PartFunc of [:X1,X2:],ExtREAL;

ex b_{1} being Function of X1,ExtREAL st

for x being Element of X1 holds b_{1} . x = Integral (M2,(ProjPMap1 (f,x)))

for b_{1}, b_{2} being Function of X1,ExtREAL st ( for x being Element of X1 holds b_{1} . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for x being Element of X1 holds b_{2} . x = Integral (M2,(ProjPMap1 (f,x))) ) holds

b_{1} = b_{2}

end;
let S2 be SigmaField of X2;

let M2 be sigma_Measure of S2;

let f be PartFunc of [:X1,X2:],ExtREAL;

func Integral2 (M2,f) -> Function of X1,ExtREAL means :Def8: :: MESFUN12:def 8

for x being Element of X1 holds it . x = Integral (M2,(ProjPMap1 (f,x)));

existence for x being Element of X1 holds it . x = Integral (M2,(ProjPMap1 (f,x)));

ex b

for x being Element of X1 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines Integral2 MESFUN12:def 8 :

for X1, X2 being non empty set

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for f being PartFunc of [:X1,X2:],ExtREAL

for b_{6} being Function of X1,ExtREAL holds

( b_{6} = Integral2 (M2,f) iff for x being Element of X1 holds b_{6} . x = Integral (M2,(ProjPMap1 (f,x))) );

for X1, X2 being non empty set

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for f being PartFunc of [:X1,X2:],ExtREAL

for b

( b

theorem Th59: :: MESFUN12:59

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for f being PartFunc of [:X1,X2:],ExtREAL

for E being Element of sigma (measurable_rectangles (S1,S2))

for V being Element of S2 st M1 is sigma_finite & ( f is nonnegative or f is nonpositive ) & E = dom f & f is_measurable_on E holds

Integral1 (M1,f) is_measurable_on V

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for f being PartFunc of [:X1,X2:],ExtREAL

for E being Element of sigma (measurable_rectangles (S1,S2))

for V being Element of S2 st M1 is sigma_finite & ( f is nonnegative or f is nonpositive ) & E = dom f & f is_measurable_on E holds

Integral1 (M1,f) is_measurable_on V

proof end;

theorem Th60: :: MESFUN12:60

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for f being PartFunc of [:X1,X2:],ExtREAL

for E being Element of sigma (measurable_rectangles (S1,S2))

for U being Element of S1 st M2 is sigma_finite & ( f is nonnegative or f is nonpositive ) & E = dom f & f is_measurable_on E holds

Integral2 (M2,f) is_measurable_on U

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for f being PartFunc of [:X1,X2:],ExtREAL

for E being Element of sigma (measurable_rectangles (S1,S2))

for U being Element of S1 st M2 is sigma_finite & ( f is nonnegative or f is nonpositive ) & E = dom f & f is_measurable_on E holds

Integral2 (M2,f) is_measurable_on U

proof end;

theorem Th61: :: MESFUN12:61

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for y being Element of X2

for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds

(X-vol (E,M1)) . y = Integral (M1,(chi ((Measurable-Y-section (E,y)),X1)))

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for y being Element of X2

for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds

(X-vol (E,M1)) . y = Integral (M1,(chi ((Measurable-Y-section (E,y)),X1)))

proof end;

theorem Th62: :: MESFUN12:62

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for x being Element of X1

for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds

(Y-vol (E,M2)) . x = Integral (M2,(chi ((Measurable-X-section (E,x)),X2)))

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for x being Element of X1

for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds

(Y-vol (E,M2)) . x = Integral (M2,(chi ((Measurable-X-section (E,x)),X2)))

proof end;

theorem Th63: :: MESFUN12:63

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for E being Element of sigma (measurable_rectangles (S1,S2))

for x being Element of X1

for y being Element of X2 holds

( ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((Measurable-X-section (E,x)),X2) & ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Measurable-Y-section (E,y)),X1) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for E being Element of sigma (measurable_rectangles (S1,S2))

for x being Element of X1

for y being Element of X2 holds

( ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((Measurable-X-section (E,x)),X2) & ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Measurable-Y-section (E,y)),X1) )

proof end;

theorem Th64: :: MESFUN12:64

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds

X-vol (E,M1) = Integral1 (M1,(chi (E,[:X1,X2:])))

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds

X-vol (E,M1) = Integral1 (M1,(chi (E,[:X1,X2:])))

proof end;

theorem Th65: :: MESFUN12:65

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds

Y-vol (E,M2) = Integral2 (M2,(chi (E,[:X1,X2:])))

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds

Y-vol (E,M2) = Integral2 (M2,(chi (E,[:X1,X2:])))

proof end;

definition

let X1, X2 be non empty set ;

let S1 be SigmaField of X1;

let S2 be SigmaField of X2;

let M1 be sigma_Measure of S1;

let M2 be sigma_Measure of S2;

coherence

product_sigma_Measure (M1,M2) is sigma_Measure of (sigma (measurable_rectangles (S1,S2)));

by MEASUR11:8;

end;
let S1 be SigmaField of X1;

let S2 be SigmaField of X2;

let M1 be sigma_Measure of S1;

let M2 be sigma_Measure of S2;

func Prod_Measure (M1,M2) -> sigma_Measure of (sigma (measurable_rectangles (S1,S2))) equals :: MESFUN12:def 9

product_sigma_Measure (M1,M2);

correctness product_sigma_Measure (M1,M2);

coherence

product_sigma_Measure (M1,M2) is sigma_Measure of (sigma (measurable_rectangles (S1,S2)));

by MEASUR11:8;

:: deftheorem defines Prod_Measure MESFUN12:def 9 :

for X1, X2 being 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 holds Prod_Measure (M1,M2) = product_sigma_Measure (M1,M2);

for X1, X2 being 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 holds Prod_Measure (M1,M2) = product_sigma_Measure (M1,M2);

theorem Th66: :: MESFUN12:66

for X1, X2 being 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 nonnegative & f is_measurable_on E1 holds

( Integral1 (M1,f) is V112() & Integral1 (M1,(f | E2)) is V112() & Integral2 (M2,f) is V112() & Integral2 (M2,(f | E2)) is V112() )

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 nonnegative & f is_measurable_on E1 holds

( Integral1 (M1,f) is V112() & Integral1 (M1,(f | E2)) is V112() & Integral2 (M2,f) is V112() & Integral2 (M2,(f | E2)) is V112() )

proof end;

theorem Th67: :: MESFUN12:67

for X1, X2 being 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_measurable_on E1 holds

( Integral1 (M1,f) is nonpositive & Integral1 (M1,(f | E2)) is nonpositive & Integral2 (M2,f) is nonpositive & Integral2 (M2,(f | E2)) is nonpositive )

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_measurable_on E1 holds

( Integral1 (M1,f) is nonpositive & Integral1 (M1,(f | E2)) is nonpositive & Integral2 (M2,f) is nonpositive & Integral2 (M2,(f | E2)) is nonpositive )

proof end;

theorem Th68: :: MESFUN12:68

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for f being PartFunc of [:X1,X2:],ExtREAL

for E1, E2 being Element of sigma (measurable_rectangles (S1,S2))

for V being Element of S2 st M1 is sigma_finite & ( f is nonnegative or f is nonpositive ) & E1 = dom f & f is_measurable_on E1 holds

Integral1 (M1,(f | E2)) is_measurable_on V

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for f being PartFunc of [:X1,X2:],ExtREAL

for E1, E2 being Element of sigma (measurable_rectangles (S1,S2))

for V being Element of S2 st M1 is sigma_finite & ( f is nonnegative or f is nonpositive ) & E1 = dom f & f is_measurable_on E1 holds

Integral1 (M1,(f | E2)) is_measurable_on V

proof end;

theorem Th69: :: MESFUN12:69

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

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

for U being Element of S1 st M2 is sigma_finite & ( f is nonnegative or f is nonpositive ) & E1 = dom f & f is_measurable_on E1 holds

Integral2 (M2,(f | E2)) is_measurable_on U

for S1 being SigmaField of X1

for S2 being SigmaField of X2

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

for U being Element of S1 st M2 is sigma_finite & ( f is nonnegative or f is nonpositive ) & E1 = dom f & f is_measurable_on E1 holds

Integral2 (M2,(f | E2)) is_measurable_on U

proof end;

theorem :: MESFUN12:70

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for f being PartFunc of [:X1,X2:],ExtREAL

for E being Element of sigma (measurable_rectangles (S1,S2))

for y being Element of X2 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is_measurable_on E & ( for x being Element of X1 st x in dom (ProjPMap2 (f,y)) holds

(ProjPMap2 (f,y)) . x = 0 ) holds

(Integral1 (M1,f)) . y = 0

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for f being PartFunc of [:X1,X2:],ExtREAL

for E being Element of sigma (measurable_rectangles (S1,S2))

for y being Element of X2 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is_measurable_on E & ( for x being Element of X1 st x in dom (ProjPMap2 (f,y)) holds

(ProjPMap2 (f,y)) . x = 0 ) holds

(Integral1 (M1,f)) . y = 0

proof end;

theorem :: MESFUN12:71

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for f being PartFunc of [:X1,X2:],ExtREAL

for E being Element of sigma (measurable_rectangles (S1,S2))

for x being Element of X1 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is_measurable_on E & ( for y being Element of X2 st y in dom (ProjPMap1 (f,x)) holds

(ProjPMap1 (f,x)) . y = 0 ) holds

(Integral2 (M2,f)) . x = 0

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for f being PartFunc of [:X1,X2:],ExtREAL

for E being Element of sigma (measurable_rectangles (S1,S2))

for x being Element of X1 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is_measurable_on E & ( for y being Element of X2 st y in dom (ProjPMap1 (f,x)) holds

(ProjPMap1 (f,x)) . y = 0 ) holds

(Integral2 (M2,f)) . x = 0

proof end;

Lm11: for X1, X2 being 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 E, A, B being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonnegative & f is_measurable_on E & A misses B holds

( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )

proof end;

Lm12: for X1, X2 being 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 E, A, B being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonpositive & f is_measurable_on E & A misses B holds

( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )

proof end;

theorem :: MESFUN12:72

for X1, X2 being 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 E, E1, E2 being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & ( f is nonnegative or f is nonpositive ) & f is_measurable_on E & E1 misses E2 holds

( Integral1 (M1,(f | (E1 \/ E2))) = (Integral1 (M1,(f | E1))) + (Integral1 (M1,(f | E2))) & Integral2 (M2,(f | (E1 \/ E2))) = (Integral2 (M2,(f | E1))) + (Integral2 (M2,(f | E2))) ) by Lm11, Lm12;

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, E1, E2 being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & ( f is nonnegative or f is nonpositive ) & f is_measurable_on E & E1 misses E2 holds

( Integral1 (M1,(f | (E1 \/ E2))) = (Integral1 (M1,(f | E1))) + (Integral1 (M1,(f | E2))) & Integral2 (M2,(f | (E1 \/ E2))) = (Integral2 (M2,(f | E1))) + (Integral2 (M2,(f | E2))) ) by Lm11, Lm12;

theorem Th73: :: MESFUN12:73

for X1, X2 being 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 E being Element of sigma (measurable_rectangles (S1,S2)) st E = dom f & f is_measurable_on E holds

( Integral1 (M1,(- f)) = - (Integral1 (M1,f)) & Integral2 (M2,(- f)) = - (Integral2 (M2,f)) )

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 E being Element of sigma (measurable_rectangles (S1,S2)) st E = dom f & f is_measurable_on E holds

( Integral1 (M1,(- f)) = - (Integral1 (M1,f)) & Integral2 (M2,(- f)) = - (Integral2 (M2,f)) )

proof end;

theorem Th74: :: MESFUN12:74

for X1, X2 being 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, g being PartFunc of [:X1,X2:],ExtREAL

for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonnegative & f is_measurable_on E1 & E2 = dom g & g is nonnegative & g is_measurable_on E2 holds

( Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) )

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, g being PartFunc of [:X1,X2:],ExtREAL

for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonnegative & f is_measurable_on E1 & E2 = dom g & g is nonnegative & g is_measurable_on E2 holds

( Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) )

proof end;

theorem :: MESFUN12:75

for X1, X2 being 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, g 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_measurable_on E1 & E2 = dom g & g is nonpositive & g is_measurable_on E2 holds

( Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) )

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, g 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_measurable_on E1 & E2 = dom g & g is nonpositive & g is_measurable_on E2 holds

( Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) )

proof end;

theorem :: MESFUN12:76

for X1, X2 being 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, g being PartFunc of [:X1,X2:],ExtREAL

for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonnegative & f is_measurable_on E1 & E2 = dom g & g is nonpositive & g is_measurable_on E2 holds

( Integral1 (M1,(f - g)) = (Integral1 (M1,(f | (dom (f - g))))) - (Integral1 (M1,(g | (dom (f - g))))) & Integral1 (M1,(g - f)) = (Integral1 (M1,(g | (dom (g - f))))) - (Integral1 (M1,(f | (dom (g - f))))) & Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) - (Integral2 (M2,(g | (dom (f - g))))) & Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f))))) )

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, g being PartFunc of [:X1,X2:],ExtREAL

for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonnegative & f is_measurable_on E1 & E2 = dom g & g is nonpositive & g is_measurable_on E2 holds

( Integral1 (M1,(f - g)) = (Integral1 (M1,(f | (dom (f - g))))) - (Integral1 (M1,(g | (dom (f - g))))) & Integral1 (M1,(g - f)) = (Integral1 (M1,(g | (dom (g - f))))) - (Integral1 (M1,(f | (dom (g - f))))) & Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) - (Integral2 (M2,(g | (dom (f - g))))) & Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f))))) )

proof end;

theorem Th77: :: MESFUN12:77

for X1, X2 being 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 E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite holds

( Integral (M1,(Y-vol (E,M2))) = Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))) & Integral (M2,(X-vol (E,M1))) = Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))) )

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)) st M1 is sigma_finite & M2 is sigma_finite holds

( Integral (M1,(Y-vol (E,M2))) = Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))) & Integral (M2,(X-vol (E,M1))) = Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))) )

proof end;

theorem Th78: :: MESFUN12:78

for X1, X2 being 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 E being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL

for r being Real st E = dom f & ( f is nonnegative or f is nonpositive ) & f is_measurable_on E holds

( Integral1 (M1,(r (#) f)) = r (#) (Integral1 (M1,f)) & Integral2 (M2,(r (#) f)) = r (#) (Integral2 (M2,f)) )

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 f being PartFunc of [:X1,X2:],ExtREAL

for r being Real st E = dom f & ( f is nonnegative or f is nonpositive ) & f is_measurable_on E holds

( Integral1 (M1,(r (#) f)) = r (#) (Integral1 (M1,f)) & Integral2 (M2,(r (#) f)) = r (#) (Integral2 (M2,f)) )

proof end;

theorem Th79: :: MESFUN12:79

for X1, X2 being 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 E being Element of sigma (measurable_rectangles (S1,S2)) holds

( Integral1 (M1,((chi (E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (E,[:X1,X2:]))) & Integral2 (M2,((chi (E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (E,[:X1,X2:]))) )

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

( Integral1 (M1,((chi (E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (E,[:X1,X2:]))) & Integral2 (M2,((chi (E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (E,[:X1,X2:]))) )

proof end;

theorem Th80: :: MESFUN12:80

for X1, X2 being 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 E being Element of sigma (measurable_rectangles (S1,S2)) holds

( Integral1 (M1,((Xchi (E,[:X1,X2:])) | E)) = Integral1 (M1,(Xchi (E,[:X1,X2:]))) & Integral2 (M2,((Xchi (E,[:X1,X2:])) | E)) = Integral2 (M2,(Xchi (E,[:X1,X2:]))) )

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

( Integral1 (M1,((Xchi (E,[:X1,X2:])) | E)) = Integral1 (M1,(Xchi (E,[:X1,X2:]))) & Integral2 (M2,((Xchi (E,[:X1,X2:])) | E)) = Integral2 (M2,(Xchi (E,[:X1,X2:]))) )

proof end;

theorem Th81: :: MESFUN12:81

for X1, X2 being 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 E being Element of sigma (measurable_rectangles (S1,S2))

for er being ExtReal holds

( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )

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 er being ExtReal holds

( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )

proof end;

theorem Th82: :: MESFUN12:82

for X1, X2 being 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 E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite holds

( Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (E,[:X1,X2:])) | E)))) )

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)) st M1 is sigma_finite & M2 is sigma_finite holds

( Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (E,[:X1,X2:])) | E)))) )

proof end;

theorem Th83: :: MESFUN12:83

for X1, X2 being 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 E being Element of sigma (measurable_rectangles (S1,S2))

for r being Real st M1 is sigma_finite & M2 is sigma_finite holds

( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )

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 r being Real st M1 is sigma_finite & M2 is sigma_finite holds

( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )

proof end;

Lm13: for X1, X2 being 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 non empty PartFunc of [:X1,X2:],ExtREAL

for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds

( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )

proof end;

Lm14: for X1, X2 being 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 empty PartFunc of [:X1,X2:],ExtREAL

for A being Element of sigma (measurable_rectangles (S1,S2)) holds

( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )

proof end;

Lm15: for X1, X2 being 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 A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds

( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )

proof end;

Lm16: for X1, X2 being 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 A being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is_measurable_on A holds

Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f)))

proof end;

Lm17: for X1, X2 being 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 A being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is_measurable_on A holds

Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f)))

proof end;

Lm18: for X1, X2 being 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 A being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonpositive & A = dom f & f is_measurable_on A holds

Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f)))

proof end;

Lm19: for X1, X2 being 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 A being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonpositive & A = dom f & f is_measurable_on A holds

Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f)))

proof end;

theorem :: MESFUN12:84

for X1, X2 being 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 A being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & ( f is nonnegative or f is nonpositive ) & A = dom f & f is_measurable_on A holds

( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) by Lm16, Lm18, Lm17, Lm19;

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 A being Element of sigma (measurable_rectangles (S1,S2))

for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & ( f is nonnegative or f is nonpositive ) & A = dom f & f is_measurable_on A holds

( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) by Lm16, Lm18, Lm17, Lm19;