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

proof

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

end;

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

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

suppose x in A ; :: thesis: (M2 . B) * ((chi (A,X1)) . x) = Integral (M2,(ProjMap1 ((chi ([:A,B:],[:X1,X2:])),x)))

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

proof

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

end;

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

end;

suppose not x in A ; :: thesis: (M2 . B) * ((chi (A,X1)) . x) = Integral (M2,(ProjMap1 ((chi ([:A,B:],[:X1,X2:])),x)))

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

proof

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

end;

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

end;

end;