:: by Noboru Endou

::

:: Received February 23, 2017

:: Copyright (c) 2017-2021 Association of Mizar Users

theorem Th72: :: MEASUR11:1

for F being disjoint_valued FinSequence

for n, m being Nat st n < m holds

union (rng (F | n)) misses F . m

for n, m being Nat st n < m holds

union (rng (F | n)) misses F . m

proof end;

theorem Th74: :: MEASUR11:3

for F being FinSequence

for n being Nat holds (union (rng (F | n))) \/ (F . (n + 1)) = union (rng (F | (n + 1)))

for n being Nat holds (union (rng (F | n))) \/ (F . (n + 1)) = union (rng (F | (n + 1)))

proof end;

theorem Th41: :: MEASUR11:5

for P being set

for F being FinSequence st P is cup-closed & {} in P & ( for n being Nat st n in dom F holds

F . n in P ) holds

Union F in P

for F being FinSequence st P is cup-closed & {} in P & ( for n being Nat st n in dom F holds

F . n in P ) holds

Union F in P

proof end;

definition

let A, X be set ;

:: original: chi

redefine func chi (A,X) -> Function of X,ExtREAL;

coherence

chi (A,X) is Function of X,ExtREAL

end;
:: original: chi

redefine func chi (A,X) -> Function of X,ExtREAL;

coherence

chi (A,X) is Function of X,ExtREAL

proof end;

definition

let X be non empty set ;

let S be SigmaField of X;

let F be FinSequence of S;

:: original: Union

redefine func Union F -> Element of S;

coherence

Union F is Element of S by PROB_3:57;

end;
let S be SigmaField of X;

let F be FinSequence of S;

:: original: Union

redefine func Union F -> Element of S;

coherence

Union F is Element of S by PROB_3:57;

definition

let X be non empty set ;

let S be SigmaField of X;

let F be sequence of S;

:: original: Union

redefine func Union F -> Element of S;

coherence

Union F is Element of S

end;
let S be SigmaField of X;

let F be sequence of S;

:: original: Union

redefine func Union F -> Element of S;

coherence

Union F is Element of S

proof end;

definition

let X be non empty set ;

let F be FinSequence of PFuncs (X,ExtREAL);

let x be Element of X;

ex b_{1} being FinSequence of ExtREAL st

( dom b_{1} = dom F & ( for n being Element of NAT st n in dom b_{1} holds

b_{1} . n = (F . n) . x ) )

for b_{1}, b_{2} being FinSequence of ExtREAL st dom b_{1} = dom F & ( for n being Element of NAT st n in dom b_{1} holds

b_{1} . n = (F . n) . x ) & dom b_{2} = dom F & ( for n being Element of NAT st n in dom b_{2} holds

b_{2} . n = (F . n) . x ) holds

b_{1} = b_{2}

end;
let F be FinSequence of PFuncs (X,ExtREAL);

let x be Element of X;

func F # x -> FinSequence of ExtREAL means :DEF5: :: MEASUR11:def 1

( dom it = dom F & ( for n being Element of NAT st n in dom it holds

it . n = (F . n) . x ) );

existence ( dom it = dom F & ( for n being Element of NAT st n in dom it holds

it . n = (F . n) . x ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem DEF5 defines # MEASUR11:def 1 :

for X being non empty set

for F being FinSequence of PFuncs (X,ExtREAL)

for x being Element of X

for b_{4} being FinSequence of ExtREAL holds

( b_{4} = F # x iff ( dom b_{4} = dom F & ( for n being Element of NAT st n in dom b_{4} holds

b_{4} . n = (F . n) . x ) ) );

for X being non empty set

for F being FinSequence of PFuncs (X,ExtREAL)

for x being Element of X

for b

( b

b

theorem :: MEASUR11:6

for X being non empty set

for S being non empty Subset-Family of X

for f being FinSequence of S

for F being FinSequence of PFuncs (X,ExtREAL) st dom f = dom F & f is disjoint_valued & ( for n being Nat st n in dom F holds

F . n = chi ((f . n),X) ) holds

for x being Element of X holds (chi ((Union f),X)) . x = Sum (F # x)

for S being non empty Subset-Family of X

for f being FinSequence of S

for F being FinSequence of PFuncs (X,ExtREAL) st dom f = dom F & f is disjoint_valued & ( for n being Nat st n in dom F holds

F . n = chi ((f . n),X) ) holds

for x being Element of X holds (chi ((Union f),X)) . x = Sum (F # x)

proof end;

theorem Th1: :: MEASUR11:7

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2 holds sigma (DisUnion (measurable_rectangles (S1,S2))) = sigma (measurable_rectangles (S1,S2))

for S1 being SigmaField of X1

for S2 being SigmaField of X2 holds sigma (DisUnion (measurable_rectangles (S1,S2))) = sigma (measurable_rectangles (S1,S2))

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;

ex b_{1} being induced_Measure of measurable_rectangles (S1,S2), product-pre-Measure (M1,M2) st

for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds

for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds

b_{1} . E = Sum ((product-pre-Measure (M1,M2)) * F)

for b_{1}, b_{2} being induced_Measure of measurable_rectangles (S1,S2), product-pre-Measure (M1,M2) st ( for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds

for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds

b_{1} . E = Sum ((product-pre-Measure (M1,M2)) * F) ) & ( for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds

for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds

b_{2} . E = Sum ((product-pre-Measure (M1,M2)) * F) ) holds

b_{1} = b_{2}

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 product_Measure (M1,M2) -> induced_Measure of measurable_rectangles (S1,S2), product-pre-Measure (M1,M2) means :: MEASUR11:def 2

for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds

for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds

it . E = Sum ((product-pre-Measure (M1,M2)) * F);

existence for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds

for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds

it . E = Sum ((product-pre-Measure (M1,M2)) * F);

ex b

for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds

for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds

b

proof end;

uniqueness for b

for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds

b

for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds

b

b

proof end;

:: deftheorem defines product_Measure MEASUR11:def 2 :

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 b_{7} being induced_Measure of measurable_rectangles (S1,S2), product-pre-Measure (M1,M2) holds

( b_{7} = product_Measure (M1,M2) iff for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds

for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds

b_{7} . E = Sum ((product-pre-Measure (M1,M2)) * F) );

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 b

( b

for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds

b

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

(sigma_Meas (C_Meas (product_Measure (M1,M2)))) | (sigma (measurable_rectangles (S1,S2))) is induced_sigma_Measure of measurable_rectangles (S1,S2), product_Measure (M1,M2);

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 product_sigma_Measure (M1,M2) -> induced_sigma_Measure of measurable_rectangles (S1,S2), product_Measure (M1,M2) equals :: MEASUR11:def 3

(sigma_Meas (C_Meas (product_Measure (M1,M2)))) | (sigma (measurable_rectangles (S1,S2)));

correctness (sigma_Meas (C_Meas (product_Measure (M1,M2)))) | (sigma (measurable_rectangles (S1,S2)));

coherence

(sigma_Meas (C_Meas (product_Measure (M1,M2)))) | (sigma (measurable_rectangles (S1,S2))) is induced_sigma_Measure of measurable_rectangles (S1,S2), product_Measure (M1,M2);

proof end;

:: deftheorem defines product_sigma_Measure MEASUR11:def 3 :

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 product_sigma_Measure (M1,M2) = (sigma_Meas (C_Meas (product_Measure (M1,M2)))) | (sigma (measurable_rectangles (S1,S2)));

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 product_sigma_Measure (M1,M2) = (sigma_Meas (C_Meas (product_Measure (M1,M2)))) | (sigma (measurable_rectangles (S1,S2)));

theorem Th2: :: MEASUR11:8

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 product_sigma_Measure (M1,M2) is sigma_Measure of (sigma (measurable_rectangles (S1,S2)))

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 product_sigma_Measure (M1,M2) is sigma_Measure of (sigma (measurable_rectangles (S1,S2)))

proof end;

theorem Th3: :: MEASUR11:9

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for F1 being Set_Sequence of S1

for F2 being Set_Sequence of S2

for n being Nat holds [:(F1 . n),(F2 . n):] is Element of sigma (measurable_rectangles (S1,S2))

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for F1 being Set_Sequence of S1

for F2 being Set_Sequence of S2

for n being Nat holds [:(F1 . n),(F2 . n):] is Element of sigma (measurable_rectangles (S1,S2))

proof end;

theorem Th4: :: MEASUR11:10

for X1, X2 being set

for F1 being SetSequence of X1

for F2 being SetSequence of X2

for n being Nat st F1 is non-descending & F2 is non-descending holds

[:(F1 . n),(F2 . n):] c= [:(F1 . (n + 1)),(F2 . (n + 1)):]

for F1 being SetSequence of X1

for F2 being SetSequence of X2

for n being Nat st F1 is non-descending & F2 is non-descending holds

[:(F1 . n),(F2 . n):] c= [:(F1 . (n + 1)),(F2 . (n + 1)):]

proof end;

theorem Th5: :: MEASUR11:11

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 S1

for B being Element of S2 holds (product_Measure (M1,M2)) . [:A,B:] = (M1 . A) * (M2 . B)

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 S1

for B being Element of S2 holds (product_Measure (M1,M2)) . [:A,B:] = (M1 . A) * (M2 . B)

proof end;

theorem Th6: :: MEASUR11:12

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 F1 being Set_Sequence of S1

for F2 being Set_Sequence of S2

for n being Nat holds (product_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))

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 F1 being Set_Sequence of S1

for F2 being Set_Sequence of S2

for n being Nat holds (product_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))

proof end;

theorem :: MEASUR11:13

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 F1 being FinSequence of S1

for F2 being FinSequence of S2

for n being Nat st n in dom F1 & n in dom F2 holds

(product_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n)) by Th5;

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 F1 being FinSequence of S1

for F2 being FinSequence of S2

for n being Nat st n in dom F1 & n in dom F2 holds

(product_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n)) by Th5;

theorem :: MEASUR11:14

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 Subset of [:X1,X2:] holds (C_Meas (product_Measure (M1,M2))) . E = inf (Svc ((product_Measure (M1,M2)),E)) by MEASURE8:def 8;

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 Subset of [:X1,X2:] holds (C_Meas (product_Measure (M1,M2))) . E = inf (Svc ((product_Measure (M1,M2)),E)) by MEASURE8:def 8;

theorem Th9: :: MEASUR11:15

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 sigma (measurable_rectangles (S1,S2)) c= sigma_Field (C_Meas (product_Measure (M1,M2)))

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 sigma (measurable_rectangles (S1,S2)) c= sigma_Field (C_Meas (product_Measure (M1,M2)))

proof end;

theorem Th10: :: MEASUR11:16

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 A being Element of S1

for B being Element of S2 st E = [:A,B:] holds

(product_sigma_Measure (M1,M2)) . E = (M1 . A) * (M2 . B)

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 A being Element of S1

for B being Element of S2 st E = [:A,B:] holds

(product_sigma_Measure (M1,M2)) . E = (M1 . A) * (M2 . B)

proof end;

theorem :: MEASUR11:17

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 F1 being Set_Sequence of S1

for F2 being Set_Sequence of S2

for n being Nat holds (product_sigma_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))

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 F1 being Set_Sequence of S1

for F2 being Set_Sequence of S2

for n being Nat holds (product_sigma_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))

proof end;

theorem Th12: :: MEASUR11:18

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

(product_sigma_Measure (M1,M2)) . (E1 \/ E2) = ((product_sigma_Measure (M1,M2)) . E1) + ((product_sigma_Measure (M1,M2)) . E2)

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

(product_sigma_Measure (M1,M2)) . (E1 \/ E2) = ((product_sigma_Measure (M1,M2)) . E1) + ((product_sigma_Measure (M1,M2)) . E2)

proof end;

theorem :: MEASUR11:19

for X1, X2, A, B being set

for F1 being SetSequence of X1

for F2 being SetSequence of X2

for F being SetSequence of [:X1,X2:] st F1 is non-descending & lim F1 = A & F2 is non-descending & lim F2 = B & ( for n being Nat holds F . n = [:(F1 . n),(F2 . n):] ) holds

lim F = [:A,B:]

for F1 being SetSequence of X1

for F2 being SetSequence of X2

for F being SetSequence of [:X1,X2:] st F1 is non-descending & lim F1 = A & F2 is non-descending & lim F2 = B & ( for n being Nat holds F . n = [:(F1 . n),(F2 . n):] ) holds

lim F = [:A,B:]

proof end;

Lm1: now :: thesis: for X, Y, x being set

for E being Subset of [:X,Y:] holds X-section (E,x) = { y where y is Element of Y : [x,y] in E }

for E being Subset of [:X,Y:] holds X-section (E,x) = { y where y is Element of Y : [x,y] in E }

let X, Y, x be set ; :: thesis: for E being Subset of [:X,Y:] holds X-section (E,x) = { y where y is Element of Y : [x,y] in E }

let E be Subset of [:X,Y:]; :: thesis: X-section (E,x) = { y where y is Element of Y : [x,y] in E }

set A = { y where y is Element of Y : [x,y] in E } ;

thus X-section (E,x) = { y where y is Element of Y : [x,y] in E } :: thesis: verum

end;
let E be Subset of [:X,Y:]; :: thesis: X-section (E,x) = { y where y is Element of Y : [x,y] in E }

set A = { y where y is Element of Y : [x,y] in E } ;

thus X-section (E,x) = { y where y is Element of Y : [x,y] in E } :: thesis: verum

proof

thus
X-section (E,x) c= { y where y is Element of Y : [x,y] in E }
:: according to XBOOLE_0:def 10 :: thesis: { y where y is Element of Y : [x,y] in E } c= X-section (E,x)

assume a in { y where y is Element of Y : [x,y] in E } ; :: thesis: a in X-section (E,x)

then consider y being Element of Y such that

A5: a = y and

A6: [x,y] in E ;

A7: x in dom E by A6, XTUPLE_0:def 12;

x in {x} by TARSKI:def 1;

hence a in X-section (E,x) by A5, A6, A7, RELAT_1:110; :: thesis: verum

end;
proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { y where y is Element of Y : [x,y] in E } or a in X-section (E,x) )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X-section (E,x) or a in { y where y is Element of Y : [x,y] in E } )

assume a in X-section (E,x) ; :: thesis: a in { y where y is Element of Y : [x,y] in E }

then consider z being object such that

z in dom E and

A2: [z,a] in E and

A3: z in {x} by RELAT_1:110;

A4: z = x by A3, TARSKI:def 1;

a in rng E by A2, XTUPLE_0:def 13;

hence a in { y where y is Element of Y : [x,y] in E } by A2, A4; :: thesis: verum

end;
assume a in X-section (E,x) ; :: thesis: a in { y where y is Element of Y : [x,y] in E }

then consider z being object such that

z in dom E and

A2: [z,a] in E and

A3: z in {x} by RELAT_1:110;

A4: z = x by A3, TARSKI:def 1;

a in rng E by A2, XTUPLE_0:def 13;

hence a in { y where y is Element of Y : [x,y] in E } by A2, A4; :: thesis: verum

assume a in { y where y is Element of Y : [x,y] in E } ; :: thesis: a in X-section (E,x)

then consider y being Element of Y such that

A5: a = y and

A6: [x,y] in E ;

A7: x in dom E by A6, XTUPLE_0:def 12;

x in {x} by TARSKI:def 1;

hence a in X-section (E,x) by A5, A6, A7, RELAT_1:110; :: thesis: verum

Lm2: now :: thesis: for X, Y, y being set

for E being Subset of [:X,Y:] holds Y-section (E,y) = { x where x is Element of X : [x,y] in E }

for E being Subset of [:X,Y:] holds Y-section (E,y) = { x where x is Element of X : [x,y] in E }

let X, Y, y be set ; :: thesis: for E being Subset of [:X,Y:] holds Y-section (E,y) = { x where x is Element of X : [x,y] in E }

let E be Subset of [:X,Y:]; :: thesis: Y-section (E,y) = { x where x is Element of X : [x,y] in E }

set A = { x where x is Element of X : [x,y] in E } ;

thus Y-section (E,y) = { x where x is Element of X : [x,y] in E } :: thesis: verum

end;
let E be Subset of [:X,Y:]; :: thesis: Y-section (E,y) = { x where x is Element of X : [x,y] in E }

set A = { x where x is Element of X : [x,y] in E } ;

thus Y-section (E,y) = { x where x is Element of X : [x,y] in E } :: thesis: verum

proof

thus
Y-section (E,y) c= { x where x is Element of X : [x,y] in E }
:: according to XBOOLE_0:def 10 :: thesis: { x where x is Element of X : [x,y] in E } c= Y-section (E,y)

assume a in { x where x is Element of X : [x,y] in E } ; :: thesis: a in Y-section (E,y)

then consider x being Element of X such that

A5: a = x and

A6: [x,y] in E ;

A7: y in rng E by A6, XTUPLE_0:def 13;

y in {y} by TARSKI:def 1;

hence a in Y-section (E,y) by A5, A6, A7, RELAT_1:131; :: thesis: verum

end;
proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { x where x is Element of X : [x,y] in E } or a in Y-section (E,y) )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Y-section (E,y) or a in { x where x is Element of X : [x,y] in E } )

assume a in Y-section (E,y) ; :: thesis: a in { x where x is Element of X : [x,y] in E }

then consider z being object such that

z in rng E and

A2: [a,z] in E and

A3: z in {y} by RELAT_1:131;

A4: z = y by A3, TARSKI:def 1;

a in dom E by A2, XTUPLE_0:def 12;

hence a in { x where x is Element of X : [x,y] in E } by A2, A4; :: thesis: verum

end;
assume a in Y-section (E,y) ; :: thesis: a in { x where x is Element of X : [x,y] in E }

then consider z being object such that

z in rng E and

A2: [a,z] in E and

A3: z in {y} by RELAT_1:131;

A4: z = y by A3, TARSKI:def 1;

a in dom E by A2, XTUPLE_0:def 12;

hence a in { x where x is Element of X : [x,y] in E } by A2, A4; :: thesis: verum

assume a in { x where x is Element of X : [x,y] in E } ; :: thesis: a in Y-section (E,y)

then consider x being Element of X such that

A5: a = x and

A6: [x,y] in E ;

A7: y in rng E by A6, XTUPLE_0:def 13;

y in {y} by TARSKI:def 1;

hence a in Y-section (E,y) by A5, A6, A7, RELAT_1:131; :: thesis: verum

definition

let X, Y be set ;

let E be Subset of [:X,Y:];

let x be set ;

X-section (E,x) is Subset of Y

for b_{1} being Subset of Y holds

( b_{1} = X-section (E,x) iff b_{1} = { y where y is Element of Y : [x,y] in E } )
by Lm1;

end;
let E be Subset of [:X,Y:];

let x be set ;

:: original: X-section

redefine func X-section (E,x) -> Subset of Y equals :: MEASUR11:def 4

{ y where y is Element of Y : [x,y] in E } ;

coherence redefine func X-section (E,x) -> Subset of Y equals :: MEASUR11:def 4

{ y where y is Element of Y : [x,y] in E } ;

X-section (E,x) is Subset of Y

proof end;

compatibility for b

( b

:: deftheorem defines X-section MEASUR11:def 4 :

for X, Y being set

for E being Subset of [:X,Y:]

for x being set holds X-section (E,x) = { y where y is Element of Y : [x,y] in E } ;

for X, Y being set

for E being Subset of [:X,Y:]

for x being set holds X-section (E,x) = { y where y is Element of Y : [x,y] in E } ;

definition

let X, Y be set ;

let E be Subset of [:X,Y:];

let y be set ;

Y-section (E,y) is Subset of X

for b_{1} being Subset of X holds

( b_{1} = Y-section (E,y) iff b_{1} = { x where x is Element of X : [x,y] in E } )
by Lm2;

end;
let E be Subset of [:X,Y:];

let y be set ;

:: original: Y-section

redefine func Y-section (E,y) -> Subset of X equals :: MEASUR11:def 5

{ x where x is Element of X : [x,y] in E } ;

coherence redefine func Y-section (E,y) -> Subset of X equals :: MEASUR11:def 5

{ x where x is Element of X : [x,y] in E } ;

Y-section (E,y) is Subset of X

proof end;

compatibility for b

( b

:: deftheorem defines Y-section MEASUR11:def 5 :

for X, Y being set

for E being Subset of [:X,Y:]

for y being set holds Y-section (E,y) = { x where x is Element of X : [x,y] in E } ;

for X, Y being set

for E being Subset of [:X,Y:]

for y being set holds Y-section (E,y) = { x where x is Element of X : [x,y] in E } ;

theorem Th16: :: MEASUR11:22

for X, Y being non empty set

for A being Subset of X

for B being Subset of Y

for p being set holds

( ( p in A implies X-section ([:A,B:],p) = B ) & ( not p in A implies X-section ([:A,B:],p) = {} ) & ( p in B implies Y-section ([:A,B:],p) = A ) & ( not p in B implies Y-section ([:A,B:],p) = {} ) )

for A being Subset of X

for B being Subset of Y

for p being set holds

( ( p in A implies X-section ([:A,B:],p) = B ) & ( not p in A implies X-section ([:A,B:],p) = {} ) & ( p in B implies Y-section ([:A,B:],p) = A ) & ( not p in B implies Y-section ([:A,B:],p) = {} ) )

proof end;

theorem Th17: :: MEASUR11:23

for X, Y being non empty set

for E being Subset of [:X,Y:]

for p being set holds

( ( not p in X implies X-section (E,p) = {} ) & ( not p in Y implies Y-section (E,p) = {} ) )

for E being Subset of [:X,Y:]

for p being set holds

( ( not p in X implies X-section (E,p) = {} ) & ( not p in Y implies Y-section (E,p) = {} ) )

proof end;

theorem :: MEASUR11:24

for X, Y being non empty set

for p being set holds

( X-section (({} [:X,Y:]),p) = {} & Y-section (({} [:X,Y:]),p) = {} & ( p in X implies X-section (([#] [:X,Y:]),p) = Y ) & ( p in Y implies Y-section (([#] [:X,Y:]),p) = X ) )

for p being set holds

( X-section (({} [:X,Y:]),p) = {} & Y-section (({} [:X,Y:]),p) = {} & ( p in X implies X-section (([#] [:X,Y:]),p) = Y ) & ( p in Y implies Y-section (([#] [:X,Y:]),p) = X ) )

proof end;

theorem Th19: :: MEASUR11:25

for X, Y being non empty set

for E being Subset of [:X,Y:]

for p being set holds

( ( p in X implies X-section (([:X,Y:] \ E),p) = Y \ (X-section (E,p)) ) & ( p in Y implies Y-section (([:X,Y:] \ E),p) = X \ (Y-section (E,p)) ) )

for E being Subset of [:X,Y:]

for p being set holds

( ( p in X implies X-section (([:X,Y:] \ E),p) = Y \ (X-section (E,p)) ) & ( p in Y implies Y-section (([:X,Y:] \ E),p) = X \ (Y-section (E,p)) ) )

proof end;

theorem Th20: :: MEASUR11:26

for X, Y being non empty set

for E1, E2 being Subset of [:X,Y:]

for p being set holds

( X-section ((E1 \/ E2),p) = (X-section (E1,p)) \/ (X-section (E2,p)) & Y-section ((E1 \/ E2),p) = (Y-section (E1,p)) \/ (Y-section (E2,p)) )

for E1, E2 being Subset of [:X,Y:]

for p being set holds

( X-section ((E1 \/ E2),p) = (X-section (E1,p)) \/ (X-section (E2,p)) & Y-section ((E1 \/ E2),p) = (Y-section (E1,p)) \/ (Y-section (E2,p)) )

proof end;

theorem Th21: :: MEASUR11:27

for X, Y being non empty set

for E1, E2 being Subset of [:X,Y:]

for p being set holds

( X-section ((E1 /\ E2),p) = (X-section (E1,p)) /\ (X-section (E2,p)) & Y-section ((E1 /\ E2),p) = (Y-section (E1,p)) /\ (Y-section (E2,p)) )

for E1, E2 being Subset of [:X,Y:]

for p being set holds

( X-section ((E1 /\ E2),p) = (X-section (E1,p)) /\ (X-section (E2,p)) & Y-section ((E1 /\ E2),p) = (Y-section (E1,p)) /\ (Y-section (E2,p)) )

proof end;

theorem Th22: :: MEASUR11:28

for X being set

for Y being non empty set

for F being FinSequence of bool [:X,Y:]

for Fy being FinSequence of bool Y

for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds

Fy . n = X-section ((F . n),p) ) holds

X-section ((union (rng F)),p) = union (rng Fy)

for Y being non empty set

for F being FinSequence of bool [:X,Y:]

for Fy being FinSequence of bool Y

for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds

Fy . n = X-section ((F . n),p) ) holds

X-section ((union (rng F)),p) = union (rng Fy)

proof end;

theorem Th23: :: MEASUR11:29

for X being non empty set

for Y being set

for F being FinSequence of bool [:X,Y:]

for Fx being FinSequence of bool X

for p being set st dom F = dom Fx & ( for n being Nat st n in dom Fx holds

Fx . n = Y-section ((F . n),p) ) holds

Y-section ((union (rng F)),p) = union (rng Fx)

for Y being set

for F being FinSequence of bool [:X,Y:]

for Fx being FinSequence of bool X

for p being set st dom F = dom Fx & ( for n being Nat st n in dom Fx holds

Fx . n = Y-section ((F . n),p) ) holds

Y-section ((union (rng F)),p) = union (rng Fx)

proof end;

theorem Th24: :: MEASUR11:30

for X being set

for Y being non empty set

for p being set

for F being SetSequence of [:X,Y:]

for Fy being SetSequence of Y st ( for n being Nat holds Fy . n = X-section ((F . n),p) ) holds

X-section ((union (rng F)),p) = union (rng Fy)

for Y being non empty set

for p being set

for F being SetSequence of [:X,Y:]

for Fy being SetSequence of Y st ( for n being Nat holds Fy . n = X-section ((F . n),p) ) holds

X-section ((union (rng F)),p) = union (rng Fy)

proof end;

theorem Th25: :: MEASUR11:31

for X being set

for Y being non empty set

for p being set

for F being SetSequence of [:X,Y:]

for Fy being SetSequence of Y st ( for n being Nat holds Fy . n = X-section ((F . n),p) ) holds

X-section ((meet (rng F)),p) = meet (rng Fy)

for Y being non empty set

for p being set

for F being SetSequence of [:X,Y:]

for Fy being SetSequence of Y st ( for n being Nat holds Fy . n = X-section ((F . n),p) ) holds

X-section ((meet (rng F)),p) = meet (rng Fy)

proof end;

theorem Th26: :: MEASUR11:32

for X being non empty set

for Y, p being set

for F being SetSequence of [:X,Y:]

for Fx being SetSequence of X st ( for n being Nat holds Fx . n = Y-section ((F . n),p) ) holds

Y-section ((union (rng F)),p) = union (rng Fx)

for Y, p being set

for F being SetSequence of [:X,Y:]

for Fx being SetSequence of X st ( for n being Nat holds Fx . n = Y-section ((F . n),p) ) holds

Y-section ((union (rng F)),p) = union (rng Fx)

proof end;

theorem Th27: :: MEASUR11:33

for X being non empty set

for Y, p being set

for F being SetSequence of [:X,Y:]

for Fx being SetSequence of X st ( for n being Nat holds Fx . n = Y-section ((F . n),p) ) holds

Y-section ((meet (rng F)),p) = meet (rng Fx)

for Y, p being set

for F being SetSequence of [:X,Y:]

for Fx being SetSequence of X st ( for n being Nat holds Fx . n = Y-section ((F . n),p) ) holds

Y-section ((meet (rng F)),p) = meet (rng Fx)

proof end;

theorem Th28: :: MEASUR11:34

for X, Y being non empty set

for x, y being set

for E being Subset of [:X,Y:] holds

( (chi (E,[:X,Y:])) . (x,y) = (chi ((X-section (E,x)),Y)) . y & (chi (E,[:X,Y:])) . (x,y) = (chi ((Y-section (E,y)),X)) . x )

for x, y being set

for E being Subset of [:X,Y:] holds

( (chi (E,[:X,Y:])) . (x,y) = (chi ((X-section (E,x)),Y)) . y & (chi (E,[:X,Y:])) . (x,y) = (chi ((Y-section (E,y)),X)) . x )

proof end;

theorem Th29: :: MEASUR11:35

for X, Y being non empty set

for E1, E2 being Subset of [:X,Y:]

for p being set st E1 misses E2 holds

( X-section (E1,p) misses X-section (E2,p) & Y-section (E1,p) misses Y-section (E2,p) )

for E1, E2 being Subset of [:X,Y:]

for p being set st E1 misses E2 holds

( X-section (E1,p) misses X-section (E2,p) & Y-section (E1,p) misses Y-section (E2,p) )

proof end;

theorem :: MEASUR11:36

for X, Y being non empty set

for F being disjoint_valued FinSequence of bool [:X,Y:]

for p being set holds

( ex Fy being disjoint_valued FinSequence of bool X st

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

Fy . n = Y-section ((F . n),p) ) ) & ex Fx being disjoint_valued FinSequence of bool Y st

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

Fx . n = X-section ((F . n),p) ) ) )

for F being disjoint_valued FinSequence of bool [:X,Y:]

for p being set holds

( ex Fy being disjoint_valued FinSequence of bool X st

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

Fy . n = Y-section ((F . n),p) ) ) & ex Fx being disjoint_valued FinSequence of bool Y st

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

Fx . n = X-section ((F . n),p) ) ) )

proof end;

theorem :: MEASUR11:37

for X, Y being non empty set

for F being V55() SetSequence of [:X,Y:]

for p being set holds

( ex Fy being V55() SetSequence of X st

for n being Nat holds Fy . n = Y-section ((F . n),p) & ex Fx being V55() SetSequence of Y st

for n being Nat holds Fx . n = X-section ((F . n),p) )

for F being V55() SetSequence of [:X,Y:]

for p being set holds

( ex Fy being V55() SetSequence of X st

for n being Nat holds Fy . n = Y-section ((F . n),p) & ex Fx being V55() SetSequence of Y st

for n being Nat holds Fx . n = X-section ((F . n),p) )

proof end;

theorem :: MEASUR11:38

for X, Y being non empty set

for x, y being set

for E1, E2 being Subset of [:X,Y:] st E1 misses E2 holds

( (chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y) & (chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x) )

for x, y being set

for E1, E2 being Subset of [:X,Y:] st E1 misses E2 holds

( (chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y) & (chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x) )

proof end;

theorem Th33: :: MEASUR11:39

for X being set

for Y being non empty set

for x being set

for E being SetSequence of [:X,Y:]

for G being SetSequence of Y st E is non-descending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds

G is non-descending

for Y being non empty set

for x being set

for E being SetSequence of [:X,Y:]

for G being SetSequence of Y st E is non-descending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds

G is non-descending

proof end;

theorem Th34: :: MEASUR11:40

for X being non empty set

for Y, x being set

for E being SetSequence of [:X,Y:]

for G being SetSequence of X st E is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) holds

G is non-descending

for Y, x being set

for E being SetSequence of [:X,Y:]

for G being SetSequence of X st E is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) holds

G is non-descending

proof end;

theorem Th35: :: MEASUR11:41

for X being set

for Y being non empty set

for x being set

for E being SetSequence of [:X,Y:]

for G being SetSequence of Y st E is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds

G is non-ascending

for Y being non empty set

for x being set

for E being SetSequence of [:X,Y:]

for G being SetSequence of Y st E is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds

G is non-ascending

proof end;

theorem Th36: :: MEASUR11:42

for X being non empty set

for Y, x being set

for E being SetSequence of [:X,Y:]

for G being SetSequence of X st E is non-ascending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) holds

G is non-ascending

for Y, x being set

for E being SetSequence of [:X,Y:]

for G being SetSequence of X st E is non-ascending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) holds

G is non-ascending

proof end;

theorem Th37: :: MEASUR11:43

for X being set

for Y being non empty set

for E being SetSequence of [:X,Y:]

for x being set st E is non-descending holds

ex G being SetSequence of Y st

( G is non-descending & ( for n being Nat holds G . n = X-section ((E . n),x) ) )

for Y being non empty set

for E being SetSequence of [:X,Y:]

for x being set st E is non-descending holds

ex G being SetSequence of Y st

( G is non-descending & ( for n being Nat holds G . n = X-section ((E . n),x) ) )

proof end;

theorem Th38: :: MEASUR11:44

for X being non empty set

for Y being set

for E being SetSequence of [:X,Y:]

for x being set st E is non-descending holds

ex G being SetSequence of X st

( G is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) )

for Y being set

for E being SetSequence of [:X,Y:]

for x being set st E is non-descending holds

ex G being SetSequence of X st

( G is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) )

proof end;

theorem Th39: :: MEASUR11:45

for X being set

for Y being non empty set

for E being SetSequence of [:X,Y:]

for x being set st E is non-ascending holds

ex G being SetSequence of Y st

( G is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) )

for Y being non empty set

for E being SetSequence of [:X,Y:]

for x being set st E is non-ascending holds

ex G being SetSequence of Y st

( G is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) )

proof end;

theorem Th40: :: MEASUR11:46

for X being non empty set

for Y being set

for E being SetSequence of [:X,Y:]

for x being set st E is non-ascending holds

ex G being SetSequence of X st

( G is non-ascending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) )

for Y being set

for E being SetSequence of [:X,Y:]

for x being set st E is non-ascending holds

ex G being SetSequence of X st

( G is non-ascending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) )

proof end;

theorem Th42: :: MEASUR11:47

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 K being set st K = { C where C is Subset of [:X1,X2:] : for p being set holds X-section (C,p) in S2 } holds

( Field_generated_by (measurable_rectangles (S1,S2)) c= K & K is SigmaField of [:X1,X2:] )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

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

for K being set st K = { C where C is Subset of [:X1,X2:] : for p being set holds X-section (C,p) in S2 } holds

( Field_generated_by (measurable_rectangles (S1,S2)) c= K & K is SigmaField of [:X1,X2:] )

proof end;

theorem Th43: :: MEASUR11:48

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 K being set st K = { C where C is Subset of [:X1,X2:] : for p being set holds Y-section (C,p) in S1 } holds

( Field_generated_by (measurable_rectangles (S1,S2)) c= K & K is SigmaField of [:X1,X2:] )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

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

for K being set st K = { C where C is Subset of [:X1,X2:] : for p being set holds Y-section (C,p) in S1 } holds

( Field_generated_by (measurable_rectangles (S1,S2)) c= K & K is SigmaField of [:X1,X2:] )

proof end;

theorem Th44: :: MEASUR11:49

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

( ( for p being set holds X-section (E,p) in S2 ) & ( for p being set holds Y-section (E,p) in S1 ) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

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

( ( for p being set holds X-section (E,p) in S2 ) & ( for p being set holds Y-section (E,p) in S1 ) )

proof end;

definition

let X1, X2 be non empty set ;

let S1 be SigmaField of X1;

let S2 be SigmaField of X2;

let E be Element of sigma (measurable_rectangles (S1,S2));

let x be set ;

correctness

coherence

X-section (E,x) is Element of S2;

by Th44;

end;
let S1 be SigmaField of X1;

let S2 be SigmaField of X2;

let E be Element of sigma (measurable_rectangles (S1,S2));

let x be set ;

correctness

coherence

X-section (E,x) is Element of S2;

by Th44;

:: deftheorem defines Measurable-X-section MEASUR11:def 6 :

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 set holds Measurable-X-section (E,x) = X-section (E,x);

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 set holds Measurable-X-section (E,x) = X-section (E,x);

definition

let X1, X2 be non empty set ;

let S1 be SigmaField of X1;

let S2 be SigmaField of X2;

let E be Element of sigma (measurable_rectangles (S1,S2));

let y be set ;

correctness

coherence

Y-section (E,y) is Element of S1;

by Th44;

end;
let S1 be SigmaField of X1;

let S2 be SigmaField of X2;

let E be Element of sigma (measurable_rectangles (S1,S2));

let y be set ;

correctness

coherence

Y-section (E,y) is Element of S1;

by Th44;

:: deftheorem defines Measurable-Y-section MEASUR11:def 7 :

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 y being set holds Measurable-Y-section (E,y) = Y-section (E,y);

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 y being set holds Measurable-Y-section (E,y) = Y-section (E,y);

theorem :: MEASUR11:50

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for F being FinSequence of sigma (measurable_rectangles (S1,S2))

for Fy being FinSequence of S2

for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds

Fy . n = Measurable-X-section ((F . n),p) ) holds

Measurable-X-section ((Union F),p) = Union Fy

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for F being FinSequence of sigma (measurable_rectangles (S1,S2))

for Fy being FinSequence of S2

for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds

Fy . n = Measurable-X-section ((F . n),p) ) holds

Measurable-X-section ((Union F),p) = Union Fy

proof end;

theorem :: MEASUR11:51

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for F being FinSequence of sigma (measurable_rectangles (S1,S2))

for Fx being FinSequence of S1

for p being set st dom F = dom Fx & ( for n being Nat st n in dom Fx holds

Fx . n = Measurable-Y-section ((F . n),p) ) holds

Measurable-Y-section ((Union F),p) = Union Fx

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for F being FinSequence of sigma (measurable_rectangles (S1,S2))

for Fx being FinSequence of S1

for p being set st dom F = dom Fx & ( for n being Nat st n in dom Fx holds

Fx . n = Measurable-Y-section ((F . n),p) ) holds

Measurable-Y-section ((Union F),p) = Union Fx

proof end;

theorem Th47: :: MEASUR11: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 A being Element of S1

for B being Element of S2

for x being Element of X1 holds (M2 . B) * ((chi (A,X1)) . x) = Integral (M2,(ProjMap1 ((chi ([:A,B:],[:X1,X2:])),x)))

for S1 being SigmaField of X1

for S2 being SigmaField of X2

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) * ((chi (A,X1)) . x) = Integral (M2,(ProjMap1 ((chi ([:A,B:],[:X1,X2:])),x)))

proof end;

theorem Th48: :: MEASUR11:53

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

for A being Element of S1

for B being Element of S2

for x being Element of X1 st E = [:A,B:] holds

M2 . (Measurable-X-section (E,x)) = (M2 . B) * ((chi (A,X1)) . x)

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

for A being Element of S1

for B being Element of S2

for x being Element of X1 st E = [:A,B:] holds

M2 . (Measurable-X-section (E,x)) = (M2 . B) * ((chi (A,X1)) . x)

proof end;

theorem Th49: :: MEASUR11:54

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 A being Element of S1

for B being Element of S2

for y being Element of X2 holds (M1 . A) * ((chi (B,X2)) . y) = Integral (M1,(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)))

for S1 being SigmaField of X1

for S2 being SigmaField of X2

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) * ((chi (B,X2)) . y) = Integral (M1,(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)))

proof end;

theorem Th50: :: MEASUR11: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 E being Element of sigma (measurable_rectangles (S1,S2))

for A being Element of S1

for B being Element of S2

for y being Element of X2 st E = [:A,B:] holds

M1 . (Measurable-Y-section (E,y)) = (M1 . A) * ((chi (B,X2)) . y)

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

for A being Element of S1

for B being Element of S2

for y being Element of X2 st E = [:A,B:] holds

M1 . (Measurable-Y-section (E,y)) = (M1 . A) * ((chi (B,X2)) . y)

proof end;

definition

let X, Y be non empty set ;

let G be FUNCTION_DOMAIN of X,Y;

let F be FinSequence of G;

let n be Nat;

:: original: /.

redefine func F /. n -> Element of G;

correctness

coherence

F /. n is Element of G;

;

end;
let G be FUNCTION_DOMAIN of X,Y;

let F be FinSequence of G;

let n be Nat;

:: original: /.

redefine func F /. n -> Element of G;

correctness

coherence

F /. n is Element of G;

;

definition

let X be set ;

let F be FinSequence of Funcs (X,ExtREAL);

end;
let F be FinSequence of Funcs (X,ExtREAL);

attr F is without_+infty-valued means :DEF10: :: MEASUR11:def 8

for n being Nat st n in dom F holds

F . n is without+infty ;

for n being Nat st n in dom F holds

F . n is without+infty ;

attr F is without_-infty-valued means :DEF11: :: MEASUR11:def 9

for n being Nat st n in dom F holds

F . n is without-infty ;

for n being Nat st n in dom F holds

F . n is without-infty ;

:: deftheorem DEF10 defines without_+infty-valued MEASUR11:def 8 :

for X being set

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

( F is without_+infty-valued iff for n being Nat st n in dom F holds

F . n is without+infty );

for X being set

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

( F is without_+infty-valued iff for n being Nat st n in dom F holds

F . n is without+infty );

:: deftheorem DEF11 defines without_-infty-valued MEASUR11:def 9 :

for X being set

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

( F is without_-infty-valued iff for n being Nat st n in dom F holds

F . n is without-infty );

for X being set

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

( F is without_-infty-valued iff for n being Nat st n in dom F holds

F . n is without-infty );

theorem Th52: :: MEASUR11:56

for X being non empty set holds

( <*(X --> 0)*> is FinSequence of Funcs (X,ExtREAL) & ( for n being Nat st n in dom <*(X --> 0)*> holds

<*(X --> 0)*> . n is without+infty ) & ( for n being Nat st n in dom <*(X --> 0)*> holds

<*(X --> 0)*> . n is without-infty ) )

( <*(X --> 0)*> is FinSequence of Funcs (X,ExtREAL) & ( for n being Nat st n in dom <*(X --> 0)*> holds

<*(X --> 0)*> . n is without+infty ) & ( for n being Nat st n in dom <*(X --> 0)*> holds

<*(X --> 0)*> . n is without-infty ) )

proof end;

registration

let X be non empty set ;

ex b_{1} being FinSequence of Funcs (X,ExtREAL) st

( b_{1} is without_+infty-valued & b_{1} is without_-infty-valued )

end;
cluster Relation-like NAT -defined Funcs (X,ExtREAL) -valued Function-like V38() FinSequence-like FinSubsequence-like without_+infty-valued without_-infty-valued for FinSequence of Funcs (X,ExtREAL);

existence ex b

( b

proof end;

theorem Th53: :: MEASUR11:57

for X being non empty set

for F being without_+infty-valued FinSequence of Funcs (X,ExtREAL)

for n being Nat st n in dom F holds

(F /. n) " {+infty} = {}

for F being without_+infty-valued FinSequence of Funcs (X,ExtREAL)

for n being Nat st n in dom F holds

(F /. n) " {+infty} = {}

proof end;

theorem Th54: :: MEASUR11:58

for X being non empty set

for F being without_-infty-valued FinSequence of Funcs (X,ExtREAL)

for n being Nat st n in dom F holds

(F /. n) " {-infty} = {}

for F being without_-infty-valued FinSequence of Funcs (X,ExtREAL)

for n being Nat st n in dom F holds

(F /. n) " {-infty} = {}

proof end;

theorem :: MEASUR11:59

for X being non empty set

for F being FinSequence of Funcs (X,ExtREAL) st ( F is without_+infty-valued or F is without_-infty-valued ) holds

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

dom ((F /. n) + (F /. m)) = X

for F being FinSequence of Funcs (X,ExtREAL) st ( F is without_+infty-valued or F is without_-infty-valued ) holds

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

dom ((F /. n) + (F /. m)) = X

proof end;

definition

let X be non empty set ;

let F be FinSequence of Funcs (X,ExtREAL);

end;
let F be FinSequence of Funcs (X,ExtREAL);

attr F is summable means :DEF12: :: MEASUR11:def 10

( F is without_+infty-valued or F is without_-infty-valued );

( F is without_+infty-valued or F is without_-infty-valued );

:: deftheorem DEF12 defines summable MEASUR11:def 10 :

for X being non empty set

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

( F is summable iff ( F is without_+infty-valued or F is without_-infty-valued ) );

for X being non empty set

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

( F is summable iff ( F is without_+infty-valued or F is without_-infty-valued ) );

registration

let X be non empty set ;

ex b_{1} being FinSequence of Funcs (X,ExtREAL) st b_{1} is summable

end;
cluster Relation-like NAT -defined Funcs (X,ExtREAL) -valued Function-like V38() FinSequence-like FinSubsequence-like summable for FinSequence of Funcs (X,ExtREAL);

existence ex b

proof end;

definition

let X be non empty set ;

let F be summable FinSequence of Funcs (X,ExtREAL);

ex b_{1} being FinSequence of Funcs (X,ExtREAL) st

( len F = len b_{1} & F . 1 = b_{1} . 1 & ( for n being Nat st 1 <= n & n < len F holds

b_{1} . (n + 1) = (b_{1} /. n) + (F /. (n + 1)) ) )

for b_{1}, b_{2} being FinSequence of Funcs (X,ExtREAL) st len F = len b_{1} & F . 1 = b_{1} . 1 & ( for n being Nat st 1 <= n & n < len F holds

b_{1} . (n + 1) = (b_{1} /. n) + (F /. (n + 1)) ) & len F = len b_{2} & F . 1 = b_{2} . 1 & ( for n being Nat st 1 <= n & n < len F holds

b_{2} . (n + 1) = (b_{2} /. n) + (F /. (n + 1)) ) holds

b_{1} = b_{2}

end;
let F be summable FinSequence of Funcs (X,ExtREAL);

func Partial_Sums F -> FinSequence of Funcs (X,ExtREAL) means :DEF13: :: MEASUR11:def 11

( len F = len it & F . 1 = it . 1 & ( for n being Nat st 1 <= n & n < len F holds

it . (n + 1) = (it /. n) + (F /. (n + 1)) ) );

existence ( len F = len it & F . 1 = it . 1 & ( for n being Nat st 1 <= n & n < len F holds

it . (n + 1) = (it /. n) + (F /. (n + 1)) ) );

ex b

( len F = len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem DEF13 defines Partial_Sums MEASUR11:def 11 :

for X being non empty set

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

for b_{3} being FinSequence of Funcs (X,ExtREAL) holds

( b_{3} = Partial_Sums F iff ( len F = len b_{3} & F . 1 = b_{3} . 1 & ( for n being Nat st 1 <= n & n < len F holds

b_{3} . (n + 1) = (b_{3} /. n) + (F /. (n + 1)) ) ) );

for X being non empty set

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

for b

( b

b

registration

let X be non empty set ;

correctness

coherence

for b_{1} being FinSequence of Funcs (X,ExtREAL) st b_{1} is without_+infty-valued holds

b_{1} is summable ;

;

correctness

coherence

for b_{1} being FinSequence of Funcs (X,ExtREAL) st b_{1} is without_-infty-valued holds

b_{1} is summable ;

;

end;
correctness

coherence

for b

b

;

correctness

coherence

for b

b

;

theorem Th56: :: MEASUR11:60

for X being non empty set

for F being without_+infty-valued FinSequence of Funcs (X,ExtREAL) holds Partial_Sums F is without_+infty-valued

for F being without_+infty-valued FinSequence of Funcs (X,ExtREAL) holds Partial_Sums F is without_+infty-valued

proof end;

theorem Th57: :: MEASUR11:61

for X being non empty set

for F being without_-infty-valued FinSequence of Funcs (X,ExtREAL) holds Partial_Sums F is without_-infty-valued

for F being without_-infty-valued FinSequence of Funcs (X,ExtREAL) holds Partial_Sums F is without_-infty-valued

proof end;

theorem :: MEASUR11:62

for X being non empty set

for A being set

for er being ExtReal

for f being Function of X,ExtREAL st ( for x being Element of X holds f . x = er * ((chi (A,X)) . x) ) holds

( ( er = +infty implies f = Xchi (A,X) ) & ( er = -infty implies f = - (Xchi (A,X)) ) & ( er <> +infty & er <> -infty implies ex r being Real st

( r = er & f = r (#) (chi (A,X)) ) ) )

for A being set

for er being ExtReal

for f being Function of X,ExtREAL st ( for x being Element of X holds f . x = er * ((chi (A,X)) . x) ) holds

( ( er = +infty implies f = Xchi (A,X) ) & ( er = -infty implies f = - (Xchi (A,X)) ) & ( er <> +infty & er <> -infty implies ex r being Real st

( r = er & f = r (#) (chi (A,X)) ) ) )

proof end;

theorem Th59: :: MEASUR11:63

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for A being Element of S st f is A -measurable & A c= dom f holds

- f is A -measurable

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for A being Element of S st f is A -measurable & A c= dom f holds

- f is A -measurable

proof end;

registration

let X be non empty set ;

let f be V175() PartFunc of X,ExtREAL;

correctness

coherence

- f is without+infty ;

end;
let f be V175() PartFunc of X,ExtREAL;

correctness

coherence

- f is without+infty ;

proof end;

registration

let X be non empty set ;

let f be V176() PartFunc of X,ExtREAL;

correctness

coherence

- f is without-infty ;

end;
let f be V176() PartFunc of X,ExtREAL;

correctness

coherence

- f is without-infty ;

proof end;

definition

let X be non empty set ;

let f1, f2 be V176() PartFunc of X,ExtREAL;

:: original: +

redefine func f1 + f2 -> V176() PartFunc of X,ExtREAL;

correctness

coherence

f1 + f2 is V176() PartFunc of X,ExtREAL;

by MESFUNC9:4;

end;
let f1, f2 be V176() PartFunc of X,ExtREAL;

:: original: +

redefine func f1 + f2 -> V176() PartFunc of X,ExtREAL;

correctness

coherence

f1 + f2 is V176() PartFunc of X,ExtREAL;

by MESFUNC9:4;

definition

let X be non empty set ;

let f1, f2 be V175() PartFunc of X,ExtREAL;

:: original: +

redefine func f1 + f2 -> V175() PartFunc of X,ExtREAL;

correctness

coherence

f1 + f2 is V175() PartFunc of X,ExtREAL;

by MESFUNC9:3;

end;
let f1, f2 be V175() PartFunc of X,ExtREAL;

:: original: +

redefine func f1 + f2 -> V175() PartFunc of X,ExtREAL;

correctness

coherence

f1 + f2 is V175() PartFunc of X,ExtREAL;

by MESFUNC9:3;

definition

let X be non empty set ;

let f1 be V176() PartFunc of X,ExtREAL;

let f2 be V175() PartFunc of X,ExtREAL;

:: original: -

redefine func f1 - f2 -> V176() PartFunc of X,ExtREAL;

correctness

coherence

f1 - f2 is V176() PartFunc of X,ExtREAL;

by MESFUNC9:6;

end;
let f1 be V176() PartFunc of X,ExtREAL;

let f2 be V175() PartFunc of X,ExtREAL;

:: original: -

redefine func f1 - f2 -> V176() PartFunc of X,ExtREAL;

correctness

coherence

f1 - f2 is V176() PartFunc of X,ExtREAL;

by MESFUNC9:6;

definition

let X be non empty set ;

let f1 be V175() PartFunc of X,ExtREAL;

let f2 be V176() PartFunc of X,ExtREAL;

:: original: -

redefine func f1 - f2 -> V175() PartFunc of X,ExtREAL;

correctness

coherence

f1 - f2 is V175() PartFunc of X,ExtREAL;

by MESFUNC9:5;

end;
let f1 be V175() PartFunc of X,ExtREAL;

let f2 be V176() PartFunc of X,ExtREAL;

:: original: -

redefine func f1 - f2 -> V175() PartFunc of X,ExtREAL;

correctness

coherence

f1 - f2 is V175() PartFunc of X,ExtREAL;

by MESFUNC9:5;

LEM10: for X being non empty set

for f being PartFunc of X,ExtREAL holds

( f " {+infty} = (- f) " {-infty} & f " {-infty} = (- f) " {+infty} )

proof end;

theorem Th60: :: MEASUR11:64

for X being non empty set

for f, g being PartFunc of X,ExtREAL holds

( - (f + g) = (- f) + (- g) & - (f - g) = (- f) + g & - (f - g) = g - f & - ((- f) + g) = f - g & - ((- f) + g) = f + (- g) )

for f, g being PartFunc of X,ExtREAL holds

( - (f + g) = (- f) + (- g) & - (f - g) = (- f) + g & - (f - g) = g - f & - ((- f) + g) = f - g & - ((- f) + g) = f + (- g) )

proof end;

theorem Th61: :: MEASUR11:65

for X being non empty set

for S being SigmaField of X

for f, g being V176() PartFunc of X,ExtREAL

for A being Element of S st f is A -measurable & g is A -measurable & A c= dom (f + g) holds

f + g is A -measurable

for S being SigmaField of X

for f, g being V176() PartFunc of X,ExtREAL

for A being Element of S st f is A -measurable & g is A -measurable & A c= dom (f + g) holds

f + g is A -measurable

proof end;

theorem :: MEASUR11:66

for X being non empty set

for S being SigmaField of X

for A being Element of S

for f being V176() PartFunc of X,ExtREAL

for g being V175() PartFunc of X,ExtREAL st f is A -measurable & g is A -measurable & A c= dom (f - g) holds

f - g is A -measurable

for S being SigmaField of X

for A being Element of S

for f being V176() PartFunc of X,ExtREAL

for g being V175() PartFunc of X,ExtREAL st f is A -measurable & g is A -measurable & A c= dom (f - g) holds

f - g is A -measurable

proof end;

theorem :: MEASUR11:67

for X being non empty set

for S being SigmaField of X

for A being Element of S

for f being V175() PartFunc of X,ExtREAL

for g being V176() PartFunc of X,ExtREAL st f is A -measurable & g is A -measurable & A c= dom (f - g) holds

f - g is A -measurable

for S being SigmaField of X

for A being Element of S

for f being V175() PartFunc of X,ExtREAL

for g being V176() PartFunc of X,ExtREAL st f is A -measurable & g is A -measurable & A c= dom (f - g) holds

f - g is A -measurable

proof end;

theorem Th64: :: MEASUR11:68

for X being non empty set

for S being SigmaField of X

for P being Element of S

for F being summable FinSequence of Funcs (X,ExtREAL) st ( for n being Nat st n in dom F holds

F /. n is P -measurable ) holds

for n being Nat st n in dom F holds

(Partial_Sums F) /. n is P -measurable

for S being SigmaField of X

for P being Element of S

for F being summable FinSequence of Funcs (X,ExtREAL) st ( for n being Nat st n in dom F holds

F /. n is P -measurable ) holds

for n being Nat st n in dom F holds

(Partial_Sums F) /. n is P -measurable

proof end;

theorem Th65: :: MEASUR11:69

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 A being Element of S1

for B being Element of S2

for x being Element of X1

for y being Element of X2 st E = [:A,B:] holds

( Integral (M2,(ProjMap1 ((chi (E,[:X1,X2:])),x))) = (M2 . (Measurable-X-section (E,x))) * ((chi (A,X1)) . x) & Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) = (M1 . (Measurable-Y-section (E,y))) * ((chi (B,X2)) . y) )

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 A being Element of S1

for B being Element of S2

for x being Element of X1

for y being Element of X2 st E = [:A,B:] holds

( Integral (M2,(ProjMap1 ((chi (E,[:X1,X2:])),x))) = (M2 . (Measurable-X-section (E,x))) * ((chi (A,X1)) . x) & Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) = (M1 . (Measurable-Y-section (E,y))) * ((chi (B,X2)) . y) )

proof end;

theorem Th66: :: MEASUR11:70

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)) st E in Field_generated_by (measurable_rectangles (S1,S2)) holds

ex f being disjoint_valued FinSequence of measurable_rectangles (S1,S2) ex A being FinSequence of S1 ex B being FinSequence of S2 st

( len f = len A & len f = len B & E = Union f & ( for n being Nat st n in dom f holds

( proj1 (f . n) = A . n & proj2 (f . n) = B . n ) ) & ( for n being Nat

for x, y being set st n in dom f & x in X1 & y in X2 holds

(chi ((f . n),[:X1,X2:])) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) ) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) holds

ex f being disjoint_valued FinSequence of measurable_rectangles (S1,S2) ex A being FinSequence of S1 ex B being FinSequence of S2 st

( len f = len A & len f = len B & E = Union f & ( for n being Nat st n in dom f holds

( proj1 (f . n) = A . n & proj2 (f . n) = B . n ) ) & ( for n being Nat

for x, y being set st n in dom f & x in X1 & y in X2 holds

(chi ((f . n),[:X1,X2:])) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) ) )

proof end;

theorem Th67: :: MEASUR11:71

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 x being Element of X1

for y being Element of X2

for U being Element of S1

for V being Element of S2 holds

( M1 . ((Measurable-Y-section (E,y)) /\ U) = Integral (M1,(ProjMap2 ((chi ((E /\ [:U,X2:]),[:X1,X2:])),y))) & M2 . ((Measurable-X-section (E,x)) /\ V) = Integral (M2,(ProjMap1 ((chi ((E /\ [:X1,V:]),[:X1,X2:])),x))) )

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 x being Element of X1

for y being Element of X2

for U being Element of S1

for V being Element of S2 holds

( M1 . ((Measurable-Y-section (E,y)) /\ U) = Integral (M1,(ProjMap2 ((chi ((E /\ [:U,X2:]),[:X1,X2:])),y))) & M2 . ((Measurable-X-section (E,x)) /\ V) = Integral (M2,(ProjMap1 ((chi ((E /\ [:X1,V:]),[:X1,X2:])),x))) )

proof end;

theorem Th68: :: MEASUR11: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 being Element of sigma (measurable_rectangles (S1,S2))

for x being Element of X1

for y being Element of X2 holds

( M1 . (Measurable-Y-section (E,y)) = Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) & M2 . (Measurable-X-section (E,x)) = Integral (M2,(ProjMap1 ((chi (E,[:X1,X2:])),x))) )

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 x being Element of X1

for y being Element of X2 holds

( M1 . (Measurable-Y-section (E,y)) = Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) & M2 . (Measurable-X-section (E,x)) = Integral (M2,(ProjMap1 ((chi (E,[:X1,X2:])),x))) )

proof end;

theorem :: MEASUR11:73

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 disjoint_valued FinSequence of measurable_rectangles (S1,S2)

for x being Element of X1

for n being Nat

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

for An being Element of S1

for Bn being Element of S2 st n in dom f & f . n = En & En = [:An,Bn:] holds

Integral (M2,(ProjMap1 ((chi ((f . n),[:X1,X2:])),x))) = (M2 . (Measurable-X-section (En,x))) * ((chi (An,X1)) . x) by Th65;

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for f being disjoint_valued FinSequence of measurable_rectangles (S1,S2)

for x being Element of X1

for n being Nat

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

for An being Element of S1

for Bn being Element of S2 st n in dom f & f . n = En & En = [:An,Bn:] holds

Integral (M2,(ProjMap1 ((chi ((f . n),[:X1,X2:])),x))) = (M2 . (Measurable-X-section (En,x))) * ((chi (An,X1)) . x) by Th65;

theorem Th70: :: MEASUR11:74

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)) st E in Field_generated_by (measurable_rectangles (S1,S2)) & E <> {} holds

ex f being disjoint_valued FinSequence of measurable_rectangles (S1,S2) ex A being FinSequence of S1 ex B being FinSequence of S2 ex Xf being summable FinSequence of Funcs ([:X1,X2:],ExtREAL) st

( E = Union f & len f in dom f & len f = len A & len f = len B & len f = len Xf & ( for n being Nat st n in dom f holds

f . n = [:(A . n),(B . n):] ) & ( for n being Nat st n in dom Xf holds

Xf . n = chi ((f . n),[:X1,X2:]) ) & (Partial_Sums Xf) . (len Xf) = chi (E,[:X1,X2:]) & ( for n being Nat

for x, y being set st n in dom Xf & x in X1 & y in X2 holds

(Xf . n) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) ) & ( for x being Element of X1 holds ProjMap1 ((chi (E,[:X1,X2:])),x) = ProjMap1 (((Partial_Sums Xf) /. (len Xf)),x) ) & ( for y being Element of X2 holds ProjMap2 ((chi (E,[:X1,X2:])),y) = ProjMap2 (((Partial_Sums Xf) /. (len Xf)),y) ) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) & E <> {} holds

ex f being disjoint_valued FinSequence of measurable_rectangles (S1,S2) ex A being FinSequence of S1 ex B being FinSequence of S2 ex Xf being summable FinSequence of Funcs ([:X1,X2:],ExtREAL) st

( E = Union f & len f in dom f & len f = len A & len f = len B & len f = len Xf & ( for n being Nat st n in dom f holds

f . n = [:(A . n),(B . n):] ) & ( for n being Nat st n in dom Xf holds

Xf . n = chi ((f . n),[:X1,X2:]) ) & (Partial_Sums Xf) . (len Xf) = chi (E,[:X1,X2:]) & ( for n being Nat

for x, y being set st n in dom Xf & x in X1 & y in X2 holds

(Xf . n) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) ) & ( for x being Element of X1 holds ProjMap1 ((chi (E,[:X1,X2:])),x) = ProjMap1 (((Partial_Sums Xf) /. (len Xf)),x) ) & ( for y being Element of X2 holds ProjMap2 ((chi (E,[:X1,X2:])),y) = ProjMap2 (((Partial_Sums Xf) /. (len Xf)),y) ) )

proof end;

theorem Th71: :: MEASUR11:75

for X1, X2 being non empty set

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for F being FinSequence of measurable_rectangles (S1,S2) holds Union F in sigma (measurable_rectangles (S1,S2))

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for F being FinSequence of measurable_rectangles (S1,S2) holds Union F in sigma (measurable_rectangles (S1,S2))

proof end;

theorem Th75: :: MEASUR11: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 E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) & E <> {} holds

ex F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) ex A being FinSequence of S1 ex B being FinSequence of S2 ex C being summable FinSequence of Funcs ([:X1,X2:],ExtREAL) ex I being summable FinSequence of Funcs (X1,ExtREAL) ex J being summable FinSequence of Funcs (X2,ExtREAL) st

( E = Union F & len F in dom F & len F = len A & len F = len B & len F = len C & len F = len I & len F = len J & ( for n being Nat st n in dom C holds

C . n = chi ((F . n),[:X1,X2:]) ) & (Partial_Sums C) /. (len C) = chi (E,[:X1,X2:]) & ( for x being Element of X1

for n being Nat st n in dom I holds

(I . n) . x = Integral (M2,(ProjMap1 ((C /. n),x))) ) & ( for n being Nat

for P being Element of S1 st n in dom I holds

I /. n is P -measurable ) & ( for x being Element of X1 holds Integral (M2,(ProjMap1 (((Partial_Sums C) /. (len C)),x))) = ((Partial_Sums I) /. (len I)) . x ) & ( for y being Element of X2

for n being Nat st n in dom J holds

(J . n) . y = Integral (M1,(ProjMap2 ((C /. n),y))) ) & ( for n being Nat

for P being Element of S2 st n in dom J holds

J /. n is P -measurable ) & ( for y being Element of X2 holds Integral (M1,(ProjMap2 (((Partial_Sums C) /. (len C)),y))) = ((Partial_Sums J) /. (len J)) . y ) )

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 E in Field_generated_by (measurable_rectangles (S1,S2)) & E <> {} holds

ex F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) ex A being FinSequence of S1 ex B being FinSequence of S2 ex C being summable FinSequence of Funcs ([:X1,X2:],ExtREAL) ex I being summable FinSequence of Funcs (X1,ExtREAL) ex J being summable FinSequence of Funcs (X2,ExtREAL) st

( E = Union F & len F in dom F & len F = len A & len F = len B & len F = len C & len F = len I & len F = len J & ( for n being Nat st n in dom C holds

C . n = chi ((F . n),[:X1,X2:]) ) & (Partial_Sums C) /. (len C) = chi (E,[:X1,X2:]) & ( for x being Element of X1

for n being Nat st n in dom I holds

(I . n) . x = Integral (M2,(ProjMap1 ((C /. n),x))) ) & ( for n being Nat

for P being Element of S1 st n in dom I holds

I /. n is P -measurable ) & ( for x being Element of X1 holds Integral (M2,(ProjMap1 (((Partial_Sums C) /. (len C)),x))) = ((Partial_Sums I) /. (len I)) . x ) & ( for y being Element of X2

for n being Nat st n in dom J holds

(J . n) . y = Integral (M1,(ProjMap2 ((C /. n),y))) ) & ( for n being Nat

for P being Element of S2 st n in dom J holds

J /. n is P -measurable ) & ( for y being Element of X2 holds Integral (M1,(ProjMap2 (((Partial_Sums C) /. (len C)),y))) = ((Partial_Sums J) /. (len J)) . y ) )

proof end;

definition

let X1, X2 be non empty set ;

let S1 be SigmaField of X1;

let S2 be SigmaField of X2;

let F be Set_Sequence of sigma (measurable_rectangles (S1,S2));

let n be Nat;

:: original: .

redefine func F . n -> Element of sigma (measurable_rectangles (S1,S2));

coherence

F . n is Element of sigma (measurable_rectangles (S1,S2)) by MEASURE8:def 2;

end;
let S1 be SigmaField of X1;

let S2 be SigmaField of X2;

let F be Set_Sequence of sigma (measurable_rectangles (S1,S2));

let n be Nat;

:: original: .

redefine func F . n -> Element of sigma (measurable_rectangles (S1,S2));

coherence

F . n is Element of sigma (measurable_rectangles (S1,S2)) by MEASURE8:def 2;

definition

let X1, X2 be non empty set ;

let S1 be SigmaField of X1;

let S2 be SigmaField of X2;

let F be Function of [:NAT,(sigma (measurable_rectangles (S1,S2))):],(sigma (measurable_rectangles (S1,S2)));

let n be Element of NAT ;

let E be Element of sigma (measurable_rectangles (S1,S2));

:: original: .

redefine func F . (n,E) -> Element of sigma (measurable_rectangles (S1,S2));

coherence

F . (n,E) is Element of sigma (measurable_rectangles (S1,S2))

end;
let S1 be SigmaField of X1;

let S2 be SigmaField of X2;

let F be Function of [:NAT,(sigma (measurable_rectangles (S1,S2))):],(sigma (measurable_rectangles (S1,S2)));

let n be Element of NAT ;

let E be Element of sigma (measurable_rectangles (S1,S2));

:: original: .

redefine func F . (n,E) -> Element of sigma (measurable_rectangles (S1,S2));

coherence

F . (n,E) is Element of sigma (measurable_rectangles (S1,S2))

proof end;

theorem Th76: :: MEASUR11: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))

for V being Element of S2 st E in Field_generated_by (measurable_rectangles (S1,S2)) holds

ex F being Function of X1,ExtREAL st

( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ V) ) & ( for P being Element of S1 holds F is P -measurable ) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for M2 being sigma_Measure of S2

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

for V being Element of S2 st E in Field_generated_by (measurable_rectangles (S1,S2)) holds

ex F being Function of X1,ExtREAL st

( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ V) ) & ( for P being Element of S1 holds F is P -measurable ) )

proof end;

theorem Th77: :: MEASUR11: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 V being Element of S1 st E in Field_generated_by (measurable_rectangles (S1,S2)) holds

ex F being Function of X2,ExtREAL st

( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for M2 being sigma_Measure of S2

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

for V being Element of S1 st E in Field_generated_by (measurable_rectangles (S1,S2)) holds

ex F being Function of X2,ExtREAL st

( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) )

proof end;

theorem Th78: :: MEASUR11:79

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 E in Field_generated_by (measurable_rectangles (S1,S2)) holds

for B being Element of S2 holds E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st

( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) }

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 E in Field_generated_by (measurable_rectangles (S1,S2)) holds

for B being Element of S2 holds E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st

( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) }

proof end;

theorem Th79: :: MEASUR11: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 E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) holds

for B being Element of S1 holds E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X2,ExtREAL st

( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ B) ) & ( for V being Element of S2 holds F is V -measurable ) ) }

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 E in Field_generated_by (measurable_rectangles (S1,S2)) holds

for B being Element of S1 holds E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X2,ExtREAL st

( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ B) ) & ( for V being Element of S2 holds F is V -measurable ) ) }

proof end;

theorem Th80: :: MEASUR11:81

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 B being Element of S2 holds Field_generated_by (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st

( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) }

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for B being Element of S2 holds Field_generated_by (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st

( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) }

proof end;

theorem Th81: :: MEASUR11: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 B being Element of S1 holds Field_generated_by (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X2,ExtREAL st

( ( for y being Element of X2 holds F . y = M1 . ((Measurable-Y-section (E,y)) /\ B) ) & ( for V being Element of S2 holds F is V -measurable ) ) }

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for B being Element of S1 holds Field_generated_by (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X2,ExtREAL st

( ( for y being Element of X2 holds F . y = M1 . ((Measurable-Y-section (E,y)) /\ B) ) & ( for V being Element of S2 holds F is V -measurable ) ) }

proof end;

definition

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

attr M is sigma_finite means :: MEASUR11:def 12

ex E being Set_Sequence of S st

( ( for n being Nat holds M . (E . n) < +infty ) & Union E = X );

ex E being Set_Sequence of S st

( ( for n being Nat holds M . (E . n) < +infty ) & Union E = X );

:: deftheorem defines sigma_finite MEASUR11:def 12 :

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S holds

( M is sigma_finite iff ex E being Set_Sequence of S st

( ( for n being Nat holds M . (E . n) < +infty ) & Union E = X ) );

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S holds

( M is sigma_finite iff ex E being Set_Sequence of S st

( ( for n being Nat holds M . (E . n) < +infty ) & Union E = X ) );

LM0902a: for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S st M is sigma_finite holds

ex F being Set_Sequence of S st

( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X )

proof end;

LM0902b: for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S st ex F being Set_Sequence of S st

( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X ) holds

M is sigma_finite

proof end;

theorem :: MEASUR11:83

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S holds

( M is sigma_finite iff ex F being Set_Sequence of S st

( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X ) ) by LM0902a, LM0902b;

for S being SigmaField of X

for M being sigma_Measure of S holds

( M is sigma_finite iff ex F being Set_Sequence of S st

( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X ) ) by LM0902a, LM0902b;

theorem :: MEASUR11:84

for X being set

for S being semialgebra_of_sets of X

for P being pre-Measure of S

for M being induced_Measure of S,P holds M = (C_Meas M) | (Field_generated_by S)

for S being semialgebra_of_sets of X

for P being pre-Measure of S

for M being induced_Measure of S,P holds M = (C_Meas M) | (Field_generated_by S)

proof end;

theorem Th84: :: MEASUR11:85

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 B being Element of S2 st M2 . B < +infty holds

{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st

( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } is MonotoneClass of [:X1,X2:]

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for B being Element of S2 st M2 . B < +infty holds

{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st

( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } is MonotoneClass of [:X1,X2:]

proof end;

theorem Th85: :: MEASUR11:86

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 B being Element of S1 st M1 . B < +infty holds

{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X2,ExtREAL st

( ( for y being Element of X2 holds F . y = M1 . ((Measurable-Y-section (E,y)) /\ B) ) & ( for V being Element of S2 holds F is V -measurable ) ) } is MonotoneClass of [:X1,X2:]

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for B being Element of S1 st M1 . B < +infty holds

{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X2,ExtREAL st

( ( for y being Element of X2 holds F . y = M1 . ((Measurable-Y-section (E,y)) /\ B) ) & ( for V being Element of S2 holds F is V -measurable ) ) } is MonotoneClass of [:X1,X2:]

proof end;

theorem :: MEASUR11:87

for X being non empty set

for F being Field_Subset of X

for L being SetSequence of X st rng L is MonotoneClass of X & F c= rng L holds

( sigma F = monotoneclass F & sigma F c= rng L )

for F being Field_Subset of X

for L being SetSequence of X st rng L is MonotoneClass of X & F c= rng L holds

( sigma F = monotoneclass F & sigma F c= rng L )

proof end;

theorem Th87: :: MEASUR11:88

for X being non empty set

for F being Field_Subset of X

for K being Subset-Family of X st K is MonotoneClass of X & F c= K holds

( sigma F = monotoneclass F & sigma F c= K )

for F being Field_Subset of X

for K being Subset-Family of X st K is MonotoneClass of X & F c= K holds

( sigma F = monotoneclass F & sigma F c= K )

proof end;

theorem Th88: :: MEASUR11:89

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 B being Element of S2 st M2 . B < +infty holds

sigma (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st

( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) }

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for B being Element of S2 st M2 . B < +infty holds

sigma (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st

( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) }

proof end;

theorem Th89: :: MEASUR11:90

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 B being Element of S1 st M1 . B < +infty holds

sigma (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X2,ExtREAL st

( ( for y being Element of X2 holds F . y = M1 . ((Measurable-Y-section (E,y)) /\ B) ) & ( for V being Element of S2 holds F is V -measurable ) ) }

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for B being Element of S1 st M1 . B < +infty holds

sigma (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X2,ExtREAL st

( ( for y being Element of X2 holds F . y = M1 . ((Measurable-Y-section (E,y)) /\ B) ) & ( for V being Element of S2 holds F is V -measurable ) ) }

proof end;

theorem Th90: :: MEASUR11:91

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

ex F being Function of X1,ExtREAL st

( ( for x being Element of X1 holds F . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds F is V -measurable ) )

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

ex F being Function of X1,ExtREAL st

( ( for x being Element of X1 holds F . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds F is V -measurable ) )

proof end;

theorem Th91: :: MEASUR11:92

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

ex F being Function of X2,ExtREAL st

( ( for y being Element of X2 holds F . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds F is V -measurable ) )

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

ex F being Function of X2,ExtREAL st

( ( for y being Element of X2 holds F . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds F is V -measurable ) )

proof end;

definition

let X1, X2 be non empty set ;

let S1 be SigmaField of X1;

let S2 be SigmaField of X2;

let M2 be sigma_Measure of S2;

let E be Element of sigma (measurable_rectangles (S1,S2));

assume A1: M2 is sigma_finite ;

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

( ( for x being Element of X1 holds b_{1} . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds b_{1} is V -measurable ) )

for b_{1}, b_{2} being V102() Function of X1,ExtREAL st ( for x being Element of X1 holds b_{1} . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds b_{1} is V -measurable ) & ( for x being Element of X1 holds b_{2} . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds b_{2} is V -measurable ) holds

b_{1} = b_{2}

end;
let S1 be SigmaField of X1;

let S2 be SigmaField of X2;

let M2 be sigma_Measure of S2;

let E be Element of sigma (measurable_rectangles (S1,S2));

assume A1: M2 is sigma_finite ;

func Y-vol (E,M2) -> V102() Function of X1,ExtREAL means :DefYvol: :: MEASUR11:def 13

( ( for x being Element of X1 holds it . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds it is V -measurable ) );

existence ( ( for x being Element of X1 holds it . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds it is V -measurable ) );

ex b

( ( for x being Element of X1 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem DefYvol defines Y-vol MEASUR11:def 13 :

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

for b_{7} being V102() Function of X1,ExtREAL holds

( b_{7} = Y-vol (E,M2) iff ( ( for x being Element of X1 holds b_{7} . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds b_{7} is V -measurable ) ) );

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

for b

( b

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 E be Element of sigma (measurable_rectangles (S1,S2));

assume A1: M1 is sigma_finite ;

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

( ( for y being Element of X2 holds b_{1} . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds b_{1} is V -measurable ) )

for b_{1}, b_{2} being V102() Function of X2,ExtREAL st ( for y being Element of X2 holds b_{1} . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds b_{1} is V -measurable ) & ( for y being Element of X2 holds b_{2} . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds b_{2} is V -measurable ) holds

b_{1} = b_{2}

end;
let S1 be SigmaField of X1;

let S2 be SigmaField of X2;

let M1 be sigma_Measure of S1;

let E be Element of sigma (measurable_rectangles (S1,S2));

assume A1: M1 is sigma_finite ;

func X-vol (E,M1) -> V102() Function of X2,ExtREAL means :DefXvol: :: MEASUR11:def 14

( ( for y being Element of X2 holds it . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds it is V -measurable ) );

existence ( ( for y being Element of X2 holds it . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds it is V -measurable ) );

ex b

( ( for y being Element of X2 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem DefXvol defines X-vol MEASUR11:def 14 :

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

for b_{7} being V102() Function of X2,ExtREAL holds

( b_{7} = X-vol (E,M1) iff ( ( for y being Element of X2 holds b_{7} . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds b_{7} is V -measurable ) ) );

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

for b

( b

theorem Th92: :: MEASUR11:93

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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite & E1 misses E2 holds

Y-vol ((E1 \/ E2),M2) = (Y-vol (E1,M2)) + (Y-vol (E2,M2))

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite & E1 misses E2 holds

Y-vol ((E1 \/ E2),M2) = (Y-vol (E1,M2)) + (Y-vol (E2,M2))

proof end;

theorem Th93: :: MEASUR11:94

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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds

X-vol ((E1 \/ E2),M1) = (X-vol (E1,M1)) + (X-vol (E2,M1))

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds

X-vol ((E1 \/ E2),M1) = (X-vol (E1,M1)) + (X-vol (E2,M1))

proof end;

theorem Th94: :: MEASUR11:95

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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite & E1 misses E2 holds

Integral (M1,(Y-vol ((E1 \/ E2),M2))) = (Integral (M1,(Y-vol (E1,M2)))) + (Integral (M1,(Y-vol (E2,M2))))

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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite & E1 misses E2 holds

Integral (M1,(Y-vol ((E1 \/ E2),M2))) = (Integral (M1,(Y-vol (E1,M2)))) + (Integral (M1,(Y-vol (E2,M2))))

proof end;

theorem Th95: :: MEASUR11:96

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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds

Integral (M2,(X-vol ((E1 \/ E2),M1))) = (Integral (M2,(X-vol (E1,M1)))) + (Integral (M2,(X-vol (E2,M1))))

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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds

Integral (M2,(X-vol ((E1 \/ E2),M1))) = (Integral (M2,(X-vol (E1,M1)))) + (Integral (M2,(X-vol (E2,M1))))

proof end;

theorem Th96: :: MEASUR11:97

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 A being Element of S1

for B being Element of S2 st E = [:A,B:] & M2 is sigma_finite holds

( ( M2 . B = +infty implies Y-vol (E,M2) = Xchi (A,X1) ) & ( M2 . B <> +infty implies ex r being Real st

( r = M2 . B & Y-vol (E,M2) = r (#) (chi (A,X1)) ) ) )

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 A being Element of S1

for B being Element of S2 st E = [:A,B:] & M2 is sigma_finite holds

( ( M2 . B = +infty implies Y-vol (E,M2) = Xchi (A,X1) ) & ( M2 . B <> +infty implies ex r being Real st

( r = M2 . B & Y-vol (E,M2) = r (#) (chi (A,X1)) ) ) )

proof end;

theorem Th97: :: MEASUR11:98

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 A being Element of S1

for B being Element of S2 st E = [:A,B:] & M1 is sigma_finite holds

( ( M1 . A = +infty implies X-vol (E,M1) = Xchi (B,X2) ) & ( M1 . A <> +infty implies ex r being Real st

( r = M1 . A & X-vol (E,M1) = r (#) (chi (B,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 A being Element of S1

for B being Element of S2 st E = [:A,B:] & M1 is sigma_finite holds

( ( M1 . A = +infty implies X-vol (E,M1) = Xchi (B,X2) ) & ( M1 . A <> +infty implies ex r being Real st

( r = M1 . A & X-vol (E,M1) = r (#) (chi (B,X2)) ) ) )

proof end;

theorem Th98: :: MEASUR11:99

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for r being Real st r >= 0 holds

Integral (M,(r (#) (chi (A,X)))) = r * (M . A)

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for r being Real st r >= 0 holds

Integral (M,(r (#) (chi (A,X)))) = r * (M . A)

proof end;

theorem Th99: :: MEASUR11:100

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

for n being Nat st M2 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds

(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M1,(Y-vol ((F . n),M2)))

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

for n being Nat st M2 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds

(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M1,(Y-vol ((F . n),M2)))

proof end;

theorem Th100: :: MEASUR11:101

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

for n being Nat st M1 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds

(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1)))

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

for n being Nat st M1 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds

(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1)))

proof end;

theorem Th102: :: MEASUR11:102

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 disjoint_valued FinSequence of sigma (measurable_rectangles (S1,S2))

for n being Nat st M2 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds

(product_sigma_Measure (M1,M2)) . (Union F) = Integral (M1,(Y-vol ((Union F),M2)))

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 disjoint_valued FinSequence of sigma (measurable_rectangles (S1,S2))

for n being Nat st M2 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds

(product_sigma_Measure (M1,M2)) . (Union F) = Integral (M1,(Y-vol ((Union F),M2)))

proof end;

theorem Th103: :: MEASUR11:103

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 disjoint_valued FinSequence of sigma (measurable_rectangles (S1,S2))

for n being Nat st M1 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds

(product_sigma_Measure (M1,M2)) . (Union F) = Integral (M2,(X-vol ((Union F),M1)))

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 disjoint_valued FinSequence of sigma (measurable_rectangles (S1,S2))

for n being Nat st M1 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds

(product_sigma_Measure (M1,M2)) . (Union F) = Integral (M2,(X-vol ((Union F),M1)))

proof end;

theorem Th104: :: MEASUR11:104

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 E in Field_generated_by (measurable_rectangles (S1,S2)) & M2 is sigma_finite holds

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

for A being Element of S1

for B being Element of S2 st V = [:A,B:] holds

E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

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 E in Field_generated_by (measurable_rectangles (S1,S2)) & M2 is sigma_finite holds

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

for A being Element of S1

for B being Element of S2 st V = [:A,B:] holds

E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

proof end;

theorem Th105: :: MEASUR11:105

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 E in Field_generated_by (measurable_rectangles (S1,S2)) & M1 is sigma_finite holds

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

for A being Element of S1

for B being Element of S2 st V = [:A,B:] holds

E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

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 E in Field_generated_by (measurable_rectangles (S1,S2)) & M1 is sigma_finite holds

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

for A being Element of S1

for B being Element of S2 st V = [:A,B:] holds

E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

proof end;

theorem Th106: :: MEASUR11:106

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

for A being Element of S1

for B being Element of S2 st M2 is sigma_finite & V = [:A,B:] holds

Field_generated_by (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

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

for A being Element of S1

for B being Element of S2 st M2 is sigma_finite & V = [:A,B:] holds

Field_generated_by (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

proof end;

theorem Th107: :: MEASUR11:107

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

for A being Element of S1

for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] holds

Field_generated_by (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

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

for A being Element of S1

for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] holds

Field_generated_by (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

proof end;

theorem Th108: :: MEASUR11:108

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

for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))

for x being Element of X1 st P is non-descending & lim P = E holds

ex K being SetSequence of S2 st

( K is non-descending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

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

for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))

for x being Element of X1 st P is non-descending & lim P = E holds

ex K being SetSequence of S2 st

( K is non-descending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )

proof end;

theorem Th109: :: MEASUR11:109

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

for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))

for y being Element of X2 st P is non-descending & lim P = E holds

ex K being SetSequence of S1 st

( K is non-descending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),y)) /\ (Measurable-Y-section (V,y)) ) & lim K = (Measurable-Y-section (E,y)) /\ (Measurable-Y-section (V,y)) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

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

for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))

for y being Element of X2 st P is non-descending & lim P = E holds

ex K being SetSequence of S1 st

( K is non-descending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),y)) /\ (Measurable-Y-section (V,y)) ) & lim K = (Measurable-Y-section (E,y)) /\ (Measurable-Y-section (V,y)) )

proof end;

theorem Th110: :: MEASUR11:110

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

for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))

for x being Element of X1 st P is non-ascending & lim P = E holds

ex K being SetSequence of S2 st

( K is non-ascending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M2 being sigma_Measure of S2

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

for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))

for x being Element of X1 st P is non-ascending & lim P = E holds

ex K being SetSequence of S2 st

( K is non-ascending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )

proof end;

theorem Th111: :: MEASUR11:111

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

for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))

for y being Element of X2 st P is non-ascending & lim P = E holds

ex K being SetSequence of S1 st

( K is non-ascending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),y)) /\ (Measurable-Y-section (V,y)) ) & lim K = (Measurable-Y-section (E,y)) /\ (Measurable-Y-section (V,y)) )

for S1 being SigmaField of X1

for S2 being SigmaField of X2

for M1 being sigma_Measure of S1

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

for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))

for y being Element of X2 st P is non-ascending & lim P = E holds

ex K being SetSequence of S1 st

( K is non-ascending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),y)) /\ (Measurable-Y-section (V,y)) ) & lim K = (Measurable-Y-section (E,y)) /\ (Measurable-Y-section (V,y)) )

proof end;

theorem Th112: :: MEASUR11:112

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

for A being Element of S1

for B being Element of S2 st M2 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M2 . B < +infty holds

{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [: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 V being Element of sigma (measurable_rectangles (S1,S2))

for A being Element of S1

for B being Element of S2 st M2 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M2 . B < +infty holds

{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:]

proof end;

theorem Th113: :: MEASUR11:113

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

for A being Element of S1

for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M1 . A < +infty holds

{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [: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 V being Element of sigma (measurable_rectangles (S1,S2))

for A being Element of S1

for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M1 . A < +infty holds

{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:]

proof end;

theorem Th114: :: MEASUR11:114

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

for A being Element of S1

for B being Element of S2 st M2 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M2 . B < +infty holds

sigma (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

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

for A being Element of S1

for B being Element of S2 st M2 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M2 . B < +infty holds

sigma (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

proof end;

theorem Th115: :: MEASUR11:115

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

for A being Element of S1

for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M1 . A < +infty holds

sigma (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

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

for A being Element of S1

for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M1 . A < +infty holds

sigma (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

proof end;

theorem Th116: :: MEASUR11:116

for X, Y being set

for A being SetSequence of X

for B being SetSequence of Y

for C being SetSequence of [:X,Y:] st A is non-descending & B is non-descending & ( for n being Nat holds C . n = [:(A . n),(B . n):] ) holds

( C is non-descending & C is convergent & Union C = [:(Union A),(Union B):] )

for A being SetSequence of X

for B being SetSequence of Y

for C being SetSequence of [:X,Y:] st A is non-descending & B is non-descending & ( for n being Nat holds C . n = [:(A . n),(B . n):] ) holds

( C is non-descending & C is convergent & Union C = [:(Union A),(Union B):] )

proof end;

:: Fubini's theorem

theorem :: MEASUR11:117

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))) = (product_sigma_Measure (M1,M2)) . 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 (M1,(Y-vol (E,M2))) = (product_sigma_Measure (M1,M2)) . E

proof end;

theorem :: MEASUR11:118

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 (M2,(X-vol (E,M1))) = (product_sigma_Measure (M1,M2)) . 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 (M2,(X-vol (E,M1))) = (product_sigma_Measure (M1,M2)) . E

proof end;