let X1, X2 be non empty set ; for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for 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)) ) ) )
let S1 be SigmaField of X1; for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for 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)) ) ) )
let S2 be 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)) ) ) )
let M1 be 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)) ) ) )
let M2 be 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)) ) ) )
let E be 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)) ) ) )
let A be 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)) ) ) )
let B be Element of S2; ( E = [:A,B:] & M2 is sigma_finite implies ( ( 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)) ) ) ) )
assume that
A1:
E = [:A,B:]
and
A2:
M2 is sigma_finite
; ( ( 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)) ) ) )
assume P1:
M2 . B <> +infty
; ex r being Real st
( r = M2 . B & Y-vol (E,M2) = r (#) (chi (A,X1)) )
M2 . B >= 0
by SUPINF_2:51;
then
M2 . B in REAL
by P1, XXREAL_0:14;
then reconsider r = M2 . B as Real ;
take
r
; ( r = M2 . B & Y-vol (E,M2) = r (#) (chi (A,X1)) )
dom (r (#) (chi (A,X1))) = dom (chi (A,X1))
by MESFUNC1:def 6;
then A8:
dom (r (#) (chi (A,X1))) = X1
by FUNCT_3:def 3;
then P2:
dom (Y-vol (E,M2)) = dom (r (#) (chi (A,X1)))
by FUNCT_2:def 1;
for x being Element of X1 st x in dom (Y-vol (E,M2)) holds
(Y-vol (E,M2)) . x = (r (#) (chi (A,X1))) . x
proof
let x be
Element of
X1;
( x in dom (Y-vol (E,M2)) implies (Y-vol (E,M2)) . x = (r (#) (chi (A,X1))) . x )
assume
x in dom (Y-vol (E,M2))
;
(Y-vol (E,M2)) . x = (r (#) (chi (A,X1))) . x
(Y-vol (E,M2)) . x =
M2 . (Measurable-X-section (E,x))
by A2, DefYvol
.=
r * ((chi (A,X1)) . x)
by A1, Th48
;
hence
(Y-vol (E,M2)) . x = (r (#) (chi (A,X1))) . x
by A8, MESFUNC1:def 6;
verum
end;
hence
( r = M2 . B & Y-vol (E,M2) = r (#) (chi (A,X1)) )
by P2, PARTFUN1:5; verum