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:] & 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)) ) ) )
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:] & 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)) ) ) )
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:] & 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)) ) ) )
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:] & 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)) ) ) )
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:] & 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)) ) ) )
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:] & 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)) ) ) )
let A be Element of S1; :: thesis: 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)) ) ) )
let B be Element of S2; :: thesis: ( E = [:A,B:] & M1 is sigma_finite implies ( ( 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)) ) ) ) )
assume that
A1: E = [:A,B:] and
A2: M1 is sigma_finite ; :: thesis: ( ( 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)) ) ) )

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

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

proof

let x be Element of X2; :: thesis: (X-vol (E,M1)) . x = (Xchi (B,X2)) . x
A4: (X-vol (E,M1)) . x = M1 . (Measurable-Y-section (E,x)) by A2, DefXvol
.= (M1 . A) * ((chi (B,X2)) . x) by A1, Th50 ;

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

suppose A5: x in B ; :: thesis: (X-vol (E,M1)) . x = (Xchi (B,X2)) . x

then (chi (B,X2)) . x = 1 by FUNCT_3:def 3;
then (X-vol (E,M1)) . x = +infty by A3, A4, XXREAL_3:81;
hence (X-vol (E,M1)) . x = (Xchi (B,X2)) . x by A5, MEASUR10:def 7; :: thesis: verum

end;

suppose A6: not x in B ; :: thesis: (X-vol (E,M1)) . x = (Xchi (B,X2)) . x

then (chi (B,X2)) . x = 0 by FUNCT_3:def 3;
then (X-vol (E,M1)) . x = 0 by A4;
hence (X-vol (E,M1)) . x = (Xchi (B,X2)) . x by A6, MEASUR10:def 7; :: thesis: verum

end;

end;

end;

hence X-vol (E,M1) = Xchi (B,X2) by FUNCT_2:def 8; :: thesis: verum

end;

assume P1: M1 . A <> +infty ; :: thesis: ex r being Real st
( r = M1 . A & X-vol (E,M1) = r (#) (chi (B,X2)) )
M1 . A >= 0 by SUPINF_2:51;
then M1 . A in REAL by P1, XXREAL_0:14;
then reconsider r = M1 . A as Real ;
take r ; :: thesis: ( r = M1 . A & X-vol (E,M1) = r (#) (chi (B,X2)) )
dom (r (#) (chi (B,X2))) = dom (chi (B,X2)) by MESFUNC1:def 6;
then A8: dom (r (#) (chi (B,X2))) = X2 by FUNCT_3:def 3;
then P2: dom (X-vol (E,M1)) = dom (r (#) (chi (B,X2))) by FUNCT_2:def 1;
for x being Element of X2 st x in dom (X-vol (E,M1)) holds
(X-vol (E,M1)) . x = (r (#) (chi (B,X2))) . x

proof

let x be Element of X2; :: thesis: ( x in dom (X-vol (E,M1)) implies (X-vol (E,M1)) . x = (r (#) (chi (B,X2))) . x )
assume x in dom (X-vol (E,M1)) ; :: thesis: (X-vol (E,M1)) . x = (r (#) (chi (B,X2))) . x
(X-vol (E,M1)) . x = M1 . (Measurable-Y-section (E,x)) by A2, DefXvol
.= r * ((chi (B,X2)) . x) by A1, Th50 ;
hence (X-vol (E,M1)) . x = (r (#) (chi (B,X2))) . x by A8, MESFUNC1:def 6; :: thesis: verum

end;

hence ( r = M1 . A & X-vol (E,M1) = r (#) (chi (B,X2)) ) by P2, PARTFUN1:5; :: thesis: verum