let x be Element of REAL ; :: thesis: for I, J, K being non empty closed_interval Subset of REAL
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom g holds
Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | (REAL \ J))) = 0
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,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | (REAL \ J))) = 0
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: ( [:[:I,J:],K:] = dom g implies Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | (REAL \ J))) = 0 )
assume A1: [:[:I,J:],K:] = dom g ; :: thesis: Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | (REAL \ J))) = 0
set Rf = R_EAL g;
set F2 = Integral2 (L-Meas,(R_EAL g));
A2: dom (R_EAL g) = [:[:I,J:],K:] by A1, MESFUNC5:def 7;
A3: dom (Integral2 (L-Meas,(R_EAL g))) = [:REAL,REAL:] by FUNCT_2:def 1;
[#] REAL = REAL by SUBSET_1:def 3;
then A4: dom (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) = REAL by A3, MESFUN16:25;
A5: J is Element of L-Field by MEASUR10:5, MEASUR12:75;
set NJ = REAL \ J;
REAL in L-Field by PROB_1:5;
then A6: REAL \ J is Element of L-Field by A5, PROB_1:6;
set RL = ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x);
reconsider RL0 = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J as PartFunc of REAL,ExtREAL ;
reconsider RL1 = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | (REAL \ J) as PartFunc of REAL,ExtREAL ;

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

let y be Element of REAL ; :: thesis: ( y in dom RL1 implies RL1 . y = 0 )
assume A7: y in dom RL1 ; :: thesis: RL1 . y = 0
( y in REAL & not y in J ) by A4, A7, XBOOLE_0:def 5;
then not [x,y] in [:I,J:] by ZFMISC_1:87;
then A8: dom (ProjPMap1 ((R_EAL g),[x,y])) = {} by A2, MESFUN16:25;
[x,y] in [:REAL,REAL:] ;
then A9: [x,y] in dom (Integral2 (L-Meas,(R_EAL g))) by FUNCT_2:def 1;
RL1 . y = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) . y by A4, A7, FUNCT_1:49;
then A10: RL1 . y = (Integral2 (L-Meas,(R_EAL g))) . (x,y) by A9, MESFUN12:def 3;
(Integral2 (L-Meas,(R_EAL g))) . (x,y) = Integral (L-Meas,(ProjPMap1 ((R_EAL g),[x,y]))) by MESFUN12:def 8;
hence RL1 . y = 0 by A8, A10, MESFUN16:1; :: thesis: verum

end;

hence Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | (REAL \ J))) = 0 by A4, A6, MESFUN12:57; :: thesis: verum