let I, J, K be non empty closed_interval Subset of REAL; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom g holds
Integral (L-Meas,((Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | (REAL \ K))) = 0
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: ( [:[:I,J:],K:] = dom g implies Integral (L-Meas,((Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | (REAL \ K))) = 0 )
assume A1: [:[:I,J:],K:] = dom g ; :: thesis: Integral (L-Meas,((Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | (REAL \ K))) = 0
set Rf = R_EAL g;
set F1 = Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g));
A2: dom (R_EAL g) = [:[:I,J:],K:] by A1, MESFUNC5:def 7;
A3: dom (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) = REAL by FUNCT_2:def 1;
A4: K is Element of L-Field by MEASUR10:5, MEASUR12:75;
set NK = REAL \ K;
REAL in L-Field by PROB_1:5;
then A5: REAL \ K is Element of L-Field by A4, PROB_1:6;
reconsider RL1 = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | (REAL \ K) as PartFunc of REAL,ExtREAL ;

now :: thesis: for z being Element of REAL st z in dom RL1 holds
RL1 . z = 0

let z be Element of REAL ; :: thesis: ( z in dom RL1 implies RL1 . z = 0 )
assume A6: z in dom RL1 ; :: thesis: RL1 . z = 0
then ( z in REAL & not z in K ) by A3, XBOOLE_0:def 5;
then A7: dom (ProjPMap2 ((R_EAL g),z)) = {} by A2, MESFUN16:26;
A8: RL1 . z = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z by A6, FUNCT_1:47;
(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z = Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 ((R_EAL g),z))) by MESFUN12:def 7;
hence RL1 . z = 0 by A7, A8, MESFUN16:1; :: thesis: verum

end;

hence Integral (L-Meas,((Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | (REAL \ K))) = 0 by A3, A5, MESFUN12:57; :: thesis: verum