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 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)))
let S1 be SigmaField of X1; :: thesis: 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)))
let S2 be SigmaField of X2; :: thesis: 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)))
let M1 be sigma_Measure of S1; :: thesis: 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)))
let A be Element of S1; :: thesis: 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)))
let B be Element of S2; :: thesis: for y being Element of X2 holds (M1 . A) * ((chi (B,X2)) . y) = Integral (M1,(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)))
let y be Element of X2; :: thesis: (M1 . A) * ((chi (B,X2)) . y) = Integral (M1,(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)))
A1: for x being Element of X1 holds (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = ((chi (A,X1)) . x) * ((chi (B,X2)) . y)

proof

let x be Element of X1; :: thesis: (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = ((chi (A,X1)) . x) * ((chi (B,X2)) . y)
(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = (chi ([:A,B:],[:X1,X2:])) . (x,y) by MESFUNC9:def 7;
hence (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = ((chi (A,X1)) . x) * ((chi (B,X2)) . y) by MEASUR10:2; :: thesis: verum

end;

set CAB = chi ([:A,B:],[:X1,X2:]);

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

suppose y in B ; :: thesis: (M1 . A) * ((chi (B,X2)) . y) = Integral (M1,(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)))

then A2: (chi (B,X2)) . y = 1 by FUNCT_3:def 3;
then A3: (M1 . A) * ((chi (B,X2)) . y) = M1 . A by XXREAL_3:81;
A4: dom (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) = X1 by FUNCT_2:def 1
.= dom (chi (A,X1)) by FUNCT_3:def 3 ;
for x being Element of X1 st x in dom (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) holds
(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = (chi (A,X1)) . x

proof

let x be Element of X1; :: thesis: ( x in dom (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) implies (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = (chi (A,X1)) . x )
assume x in dom (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) ; :: thesis: (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = (chi (A,X1)) . x
(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = ((chi (A,X1)) . x) * ((chi (B,X2)) . y) by A1;
hence (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = (chi (A,X1)) . x by A2, XXREAL_3:81; :: thesis: verum

end;

then ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y) = chi (A,X1) by A4, PARTFUN1:5;
hence (M1 . A) * ((chi (B,X2)) . y) = Integral (M1,(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y))) by A3, MESFUNC9:14; :: thesis: verum

end;

suppose not y in B ; :: thesis: (M1 . A) * ((chi (B,X2)) . y) = Integral (M1,(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)))

then A5: (chi (B,X2)) . y = 0 by FUNCT_3:def 3;
then A6: (M1 . A) * ((chi (B,X2)) . y) = 0 ;
A7: {} is Element of S1 by PROB_1:4;
A8: dom (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) = X1 by FUNCT_2:def 1
.= dom (chi ({},X1)) by FUNCT_3:def 3 ;
for x being Element of X1 st x in dom (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) holds
(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = (chi ({},X1)) . x

proof

let x be Element of X1; :: thesis: ( x in dom (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) implies (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = (chi ({},X1)) . x )
assume x in dom (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) ; :: thesis: (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = (chi ({},X1)) . x
(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = ((chi (A,X1)) . x) * ((chi (B,X2)) . y) by A1;
then (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = 0 by A5;
hence (ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)) . x = (chi ({},X1)) . x by FUNCT_3:def 3; :: thesis: verum

end;

then ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y) = chi ({},X1) by A8, PARTFUN1:5;
then Integral (M1,(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y))) = M1 . {} by A7, MESFUNC9:14;
hence (M1 . A) * ((chi (B,X2)) . y) = Integral (M1,(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y))) by A6, VALUED_0:def 19; :: thesis: verum

end;

end;