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 G1 being PartFunc of REAL,REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 (L-Meas,(R_EAL g))) | J holds
Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) = integral (G1,J)
let f be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:REAL,REAL:],REAL
for G1 being PartFunc of REAL,REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 (L-Meas,(R_EAL g))) | J holds
Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) = integral (G1,J)
let g be PartFunc of [:REAL,REAL:],REAL; :: thesis: for G1 being PartFunc of REAL,REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 (L-Meas,(R_EAL g))) | J holds
Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) = integral (G1,J)
let G1 be PartFunc of REAL,REAL; :: thesis: ( [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 (L-Meas,(R_EAL g))) | J implies Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) = integral (G1,J) )
assume that
A1: [:I,J:] = dom f and
A2: f is_continuous_on [:I,J:] and
A3: f = g and
A4: G1 = (Integral1 (L-Meas,(R_EAL g))) | J ; :: thesis: Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) = integral (G1,J)
set Rg = R_EAL g;
set NJ = REAL \ J;
set RG1 = Integral1 (L-Meas,(R_EAL g));
set F0 = (Integral1 (L-Meas,(R_EAL g))) | J;
set F1 = (Integral1 (L-Meas,(R_EAL g))) | (REAL \ J);
A5: dom (Integral1 (L-Meas,(R_EAL g))) = REAL by FUNCT_2:def 1;
then A6: dom ((Integral1 (L-Meas,(R_EAL g))) | J) = J ;
A7: J is Element of L-Field by MEASUR10:5, MEASUR12:75;
( G1 | J is bounded & G1 is_integrable_on J ) by A6, A1, A2, A3, A4, Th56, INTEGRA5:10, INTEGRA5:11;
then A8: Integral (L-Meas,(G1 | J)) = integral (G1,J) by A4, A7, A6, MESFUN14:49;
REAL in L-Field by PROB_1:5;
then A9: REAL \ J is Element of L-Field by A7, PROB_1:6;
A10: Integral ((Prod_Measure (L-Meas,L-Meas)),g) = Integral (L-Meas,(Integral1 (L-Meas,(R_EAL g)))) by A2, A1, A3, Lm5;
J \/ (REAL \ J) = REAL by XBOOLE_1:45;
then A11: (Integral1 (L-Meas,(R_EAL g))) | (J \/ (REAL \ J)) = Integral1 (L-Meas,(R_EAL g)) ;
Integral1 (L-Meas,(R_EAL g)) is_integrable_on L-Meas by A2, A1, A3, Lm5;
then A12: Integral (L-Meas,(Integral1 (L-Meas,(R_EAL g)))) = (Integral (L-Meas,((Integral1 (L-Meas,(R_EAL g))) | J))) + (Integral (L-Meas,((Integral1 (L-Meas,(R_EAL g))) | (REAL \ J)))) by A7, A9, A11, XBOOLE_1:85, MESFUNC5:98;
for y being Element of REAL st y in dom ((Integral1 (L-Meas,(R_EAL g))) | (REAL \ J)) holds
((Integral1 (L-Meas,(R_EAL g))) | (REAL \ J)) . y = 0

proof

let y be Element of REAL ; :: thesis: ( y in dom ((Integral1 (L-Meas,(R_EAL g))) | (REAL \ J)) implies ((Integral1 (L-Meas,(R_EAL g))) | (REAL \ J)) . y = 0 )
assume A13: y in dom ((Integral1 (L-Meas,(R_EAL g))) | (REAL \ J)) ; :: thesis: ((Integral1 (L-Meas,(R_EAL g))) | (REAL \ J)) . y = 0
then not y in J by XBOOLE_0:def 5;
then A14: dom (ProjPMap2 ((R_EAL g),y)) = {} by A1, A3, Th28;
(Integral1 (L-Meas,(R_EAL g))) . y = Integral (L-Meas,(ProjPMap2 ((R_EAL g),y))) by MESFUN12:def 7;
then (Integral1 (L-Meas,(R_EAL g))) . y = 0 by A14, Th1;
hence ((Integral1 (L-Meas,(R_EAL g))) | (REAL \ J)) . y = 0 by FUNCT_1:49, A13; :: thesis: verum

end;

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