let I, J be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL
for G2 being PartFunc of REAL,REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | I holds
Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) = integral (G2,I)
let f be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:REAL,REAL:],REAL
for G2 being PartFunc of REAL,REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | I holds
Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) = integral (G2,I)
let g be PartFunc of [:REAL,REAL:],REAL; :: thesis: for G2 being PartFunc of REAL,REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | I holds
Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) = integral (G2,I)
let G2 be PartFunc of REAL,REAL; :: thesis: ( [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | I implies Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) = integral (G2,I) )
assume that
A1: [:I,J:] = dom f and
A2: f is_continuous_on [:I,J:] and
A3: f = g and
A4: G2 = (Integral2 (L-Meas,(R_EAL g))) | I ; :: thesis: Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) = integral (G2,I)
set Rg = R_EAL g;
set NI = REAL \ I;
set RG2 = Integral2 (L-Meas,(R_EAL g));
set F0 = (Integral2 (L-Meas,(R_EAL g))) | I;
set F1 = (Integral2 (L-Meas,(R_EAL g))) | (REAL \ I);
A5: dom (Integral2 (L-Meas,(R_EAL g))) = REAL by FUNCT_2:def 1;
then A6: dom G2 = I by A4;
A7: I is Element of L-Field by MEASUR10:5, MEASUR12:75;
G2 is continuous by A1, A2, A3, A4, Th53;
then ( G2 | I is bounded & G2 is_integrable_on I ) by A4, A5, INTEGRA5:10, INTEGRA5:11;
then A8: Integral (L-Meas,(G2 | I)) = integral (G2,I) by A6, A7, MESFUN14:49;
REAL in L-Field by PROB_1:5;
then A9: REAL \ I is Element of L-Field by A7, PROB_1:6;
A10: Integral ((Prod_Measure (L-Meas,L-Meas)),g) = Integral (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) by A2, A1, A3, Lm4;
I \/ (REAL \ I) = REAL by XBOOLE_1:45;
then A11: (Integral2 (L-Meas,(R_EAL g))) | (I \/ (REAL \ I)) = Integral2 (L-Meas,(R_EAL g)) ;
Integral2 (L-Meas,(R_EAL g)) is_integrable_on L-Meas by A2, A3, A1, Lm4;
then A12: Integral (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) = (Integral (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | I))) + (Integral (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | (REAL \ I)))) by A7, A9, A11, XBOOLE_1:85, MESFUNC5:98;
for x being Element of REAL st x in dom ((Integral2 (L-Meas,(R_EAL g))) | (REAL \ I)) holds
((Integral2 (L-Meas,(R_EAL g))) | (REAL \ I)) . x = 0

proof

let x be Element of REAL ; :: thesis: ( x in dom ((Integral2 (L-Meas,(R_EAL g))) | (REAL \ I)) implies ((Integral2 (L-Meas,(R_EAL g))) | (REAL \ I)) . x = 0 )
assume A13: x in dom ((Integral2 (L-Meas,(R_EAL g))) | (REAL \ I)) ; :: thesis: ((Integral2 (L-Meas,(R_EAL g))) | (REAL \ I)) . x = 0
then not x in I by XBOOLE_0:def 5;
then A14: dom (ProjPMap1 ((R_EAL g),x)) = {} by A1, A3, Th27;
(Integral2 (L-Meas,(R_EAL g))) . x = Integral (L-Meas,(ProjPMap1 ((R_EAL g),x))) by MESFUN12:def 8;
then (Integral2 (L-Meas,(R_EAL g))) . x = 0 by A14, Th1;
hence ((Integral2 (L-Meas,(R_EAL g))) | (REAL \ I)) . x = 0 by A13, FUNCT_1:49; :: thesis: verum

end;

then Integral (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | (REAL \ I))) = 0 by A9, A5, MESFUN12:57;
then Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) = Integral (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | I)) by A10, A12, XXREAL_3:4;
hence Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) = integral (G2,I) by A4, A8, MESFUNC5:def 7; :: thesis: verum