let I, J, K be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
Integral2 (L-Meas,|.(R_EAL g).|) is nonnegative
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
Integral2 (L-Meas,|.(R_EAL g).|) is nonnegative
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: ( [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g implies Integral2 (L-Meas,|.(R_EAL g).|) is nonnegative )
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f is_continuous_on [:[:I,J:],K:] and
A3: f = g ; :: thesis: Integral2 (L-Meas,|.(R_EAL g).|) is nonnegative
dom (R_EAL g) = [:[:I,J:],K:] by A1, A3, MESFUNC5:def 7;
then A4: dom |.(R_EAL g).| = [:[:I,J:],K:] by MESFUNC1:def 10;

now :: thesis: for p being Element of [:REAL,REAL:] holds 0 <= (Integral2 (L-Meas,|.(R_EAL g).|)) . p

let p be Element of [:REAL,REAL:]; :: thesis: 0 <= (Integral2 (L-Meas,|.(R_EAL g).|)) . b₁

per cases ( p in [:I,J:] or not p in [:I,J:] ) ;

suppose A5: p in [:I,J:] ; :: thesis: 0 <= (Integral2 (L-Meas,|.(R_EAL g).|)) . b₁

consider x1, y1 being object such that
A6: ( x1 in REAL & y1 in REAL & p = [x1,y1] ) by ZFMISC_1:84;
reconsider x1 = x1, y1 = y1 as Element of REAL by A6;
A7: ( x1 in I & y1 in J ) by A5, A6, ZFMISC_1:87;
reconsider Pg = ProjPMap1 (|.(R_EAL g).|,p) as PartFunc of REAL,REAL by MESFUN16:30;
reconsider K0 = K as Element of L-Field by MEASUR10:5, MEASUR12:75;
A8: K is Element of L-Field by MEASUR10:5, MEASUR12:75;
A9: dom Pg = K by A1, A3, A5, MESFUN16:27;
A10: ( Pg | K is bounded & Pg is_integrable_on K ) by A7, A1, A2, A3, A6, Th24;
A11: ( Pg is_integrable_on L-Meas & integral (Pg,K) = Integral (L-Meas,Pg) ) by A8, A9, A10, MESFUN14:49;
R_EAL Pg = ProjPMap1 (|.(R_EAL g).|,p) by MESFUNC5:def 7;
then A12: (Integral2 (L-Meas,|.(R_EAL g).|)) . p = integral (Pg,K) by A11, MESFUN12:def 8;
A13: Pg is K0 -measurable by A1, A2, A3, A6, A7, Th25;
for y being object st y in dom (Pg | K) holds
0 <= (Pg | K) . y

proof

let y be object ; :: thesis: ( y in dom (Pg | K) implies 0 <= (Pg | K) . y )
assume A14: y in dom (Pg | K) ; :: thesis: 0 <= (Pg | K) . y
then y in K ;
then reconsider y = y as Element of REAL ;
A15: (ProjPMap1 (|.(R_EAL g).|,p)) . y = |.(R_EAL g).| . (p,y) by A5, A14, A4, ZFMISC_1:87, MESFUN12:def 3;
A16: (R_EAL g) . [p,y] = g . [p,y] by MESFUNC5:def 7;
|.(R_EAL g).| . (p,y) = |.((R_EAL g) . [p,y]).| by A4, A5, A14, ZFMISC_1:87, MESFUNC1:def 10;
then |.(R_EAL g).| . (p,y) = |.(g . [p,y]).| by A16, EXTREAL1:12;
hence 0 <= (Pg | K) . y by A14, A15, FUNCT_1:49; :: thesis: verum

end;

hence 0 <= (Integral2 (L-Meas,|.(R_EAL g).|)) . p by A9, A11, A12, A13, MESFUNC6:52, MESFUNC6:84; :: thesis: verum

end;

suppose not p in [:I,J:] ; :: thesis: 0 <= (Integral2 (L-Meas,|.(R_EAL g).|)) . b₁

hence 0 <= (Integral2 (L-Meas,|.(R_EAL g).|)) . p by A1, A3, Lm4; :: thesis: verum

end;

end;

end;

hence Integral2 (L-Meas,|.(R_EAL g).|) is nonnegative ; :: thesis: verum