let y 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,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | (REAL \ I))) = 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,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | (REAL \ I))) = 0
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: ( [:[:I,J:],K:] = dom g implies Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | (REAL \ I))) = 0 )
assume A1: [:[:I,J:],K:] = dom g ; :: thesis: Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | (REAL \ I))) = 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 (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) = REAL by A3, MESFUN16:26;
A5: I is Element of L-Field by MEASUR10:5, MEASUR12:75;
set NI = REAL \ I;
REAL in L-Field by PROB_1:5;
then A6: REAL \ I is Element of L-Field by A5, PROB_1:6;
set RL = ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y);
reconsider RL1 = (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | (REAL \ I) as PartFunc of REAL,ExtREAL ;

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

let x be Element of REAL ; :: thesis: ( x in dom RL1 implies RL1 . x = 0 )
assume A7: x in dom RL1 ; :: thesis: RL1 . x = 0
( x in REAL & not x in I ) 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 . x = (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) . x by A4, A7, FUNCT_1:49;
then A10: RL1 . x = (Integral2 (L-Meas,(R_EAL g))) . (x,y) by A9, MESFUN12:def 4;
(Integral2 (L-Meas,(R_EAL g))) . (x,y) = Integral (L-Meas,(ProjPMap1 ((R_EAL g),[x,y]))) by MESFUN12:def 8;
hence RL1 . x = 0 by A8, A10, MESFUN16:1; :: thesis: verum

end;

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