let X1, X2 be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( ( 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)) ) ) )

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

assume A3: M2 . B = +infty ; :: thesis: Y-vol (E,M2) = Xchi (A,X1)
for x being Element of X1 holds (Y-vol (E,M2)) . x = (Xchi (A,X1)) . x

proof

let x be Element of X1; :: thesis: (Y-vol (E,M2)) . x = (Xchi (A,X1)) . x
A4: (Y-vol (E,M2)) . x = M2 . (Measurable-X-section (E,x)) by A2, DefYvol
.= (M2 . B) * ((chi (A,X1)) . x) by A1, Th48 ;

per cases ( x in A or not x in A ) ;

suppose A5: x in A ; :: thesis: (Y-vol (E,M2)) . x = (Xchi (A,X1)) . x

then (chi (A,X1)) . x = 1 by FUNCT_3:def 3;
then (Y-vol (E,M2)) . x = +infty by A3, A4, XXREAL_3:81;
hence (Y-vol (E,M2)) . x = (Xchi (A,X1)) . x by A5, MEASUR10:def 7; :: thesis: verum

end;

suppose A6: not x in A ; :: thesis: (Y-vol (E,M2)) . x = (Xchi (A,X1)) . x

then (chi (A,X1)) . x = 0 by FUNCT_3:def 3;
then (Y-vol (E,M2)) . x = 0 by A4;
hence (Y-vol (E,M2)) . x = (Xchi (A,X1)) . x by A6, MEASUR10:def 7; :: thesis: verum

end;

end;

end;

hence Y-vol (E,M2) = Xchi (A,X1) by FUNCT_2:def 8; :: thesis: verum

end;

assume P1: M2 . B <> +infty ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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)) ; :: thesis: (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; :: thesis: verum

end;

hence ( r = M2 . B & Y-vol (E,M2) = r (#) (chi (A,X1)) ) by P2, PARTFUN1:5; :: thesis: verum