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
Integral1 ((Prod_Measure (L-Meas,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
Integral1 ((Prod_Measure (L-Meas,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 Integral1 ((Prod_Measure (L-Meas,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: Integral1 ((Prod_Measure (L-Meas,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 z being Element of REAL holds 0 <= (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z

let z be Element of REAL ; :: thesis: 0 <= (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . b₁

per cases ( z in K or not z in K ) ;

suppose A5: z in K ; :: thesis: 0 <= (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . b₁

reconsider Pg = ProjPMap2 (|.(R_EAL g).|,z) as PartFunc of [:REAL,REAL:],REAL by MESFUN16:30;
reconsider Pf = Pg as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;
reconsider IJ = [:I,J:] as Element of sigma (measurable_rectangles (L-Field,L-Field)) by MESFUN16:11;
A6: dom Pf = [:I,J:] by A1, A3, A5, MESFUN16:28;
Pf is_continuous_on dom Pf by A1, A2, A3, Th20;
then A7: ( Pg is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg) = Integral (L-Meas,(Integral2 (L-Meas,(R_EAL Pg)))) ) by A6, MESFUN16:57;
R_EAL Pg = ProjPMap2 (|.(R_EAL g).|,z) by MESFUNC5:def 7;
then A8: (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z = Integral ((Prod_Measure (L-Meas,L-Meas)),(R_EAL Pg)) by MESFUN12:def 7;
A9: Pg is IJ -measurable by A1, A2, A3, A5, Th27;
for u being object st u in dom (Pg | IJ) holds
0 <= (Pg | IJ) . u

proof

let u be object ; :: thesis: ( u in dom (Pg | IJ) implies 0 <= (Pg | IJ) . u )
assume A10: u in dom (Pg | IJ) ; :: thesis: 0 <= (Pg | IJ) . u
then u in IJ ;
then reconsider u = u as Element of [:REAL,REAL:] ;
A11: (ProjPMap2 (|.(R_EAL g).|,z)) . u = |.(R_EAL g).| . (u,z) by A5, A10, A4, ZFMISC_1:87, MESFUN12:def 4;
A12: (R_EAL g) . [u,z] = g . [u,z] by MESFUNC5:def 7;
|.(R_EAL g).| . (u,z) = |.((R_EAL g) . [u,z]).| by A4, A5, A10, ZFMISC_1:87, MESFUNC1:def 10;
then |.(R_EAL g).| . (u,z) = |.(g . [u,z]).| by A12, EXTREAL1:12;
hence 0 <= (Pg | IJ) . u by A10, A11, FUNCT_1:49; :: thesis: verum

end;

hence 0 <= (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z by A6, A7, A8, A9, MESFUNC6:52, MESFUNC6:84; :: thesis: verum

end;

suppose not z in K ; :: thesis: 0 <= (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . b₁

hence 0 <= (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z by A1, A3, Lm5; :: thesis: verum

end;

end;

end;

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