let I, J be non empty closed_interval Subset of REAL; :: thesis:
let f be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis:
let g be PartFunc of [:REAL,REAL:],REAL; :: thesis:
assume that
A1: [:I,J:] = dom f and
A2: f is_continuous_on [:I,J:] and
A3: f = g ; :: thesis:
consider E being Subset of [:RNS_Real,RNS_Real:] such that
A4: ( E = [:I,J:] & E is compact ) by Th9;
reconsider E = E as Element of sigma (measurable_rectangles (L-Field,L-Field)) by A4, Th11;
A5: g is E -measurable by A1, A2, A3, A4, Th50;
set Rg = R_EAL g;
A6: dom g = dom (R_EAL g) by MESFUNC5:def 7;
then A7: dom |.(R_EAL g).| = [:I,J:] by A1, A3, MESFUNC1:def 10;
A8: for x being Element of REAL st x in REAL \ I holds
(Integral2 (L-Meas,|.(R_EAL g).|)) . x = 0

proof

let x be Element of REAL ; :: thesis:
assume x in REAL \ I ; :: thesis:
then not x in I by XBOOLE_0:def 5;
then dom (ProjPMap1 (|.(R_EAL g).|,x)) = {} by A1, A3, Th27;
then Integral (L-Meas,(ProjPMap1 (|.(R_EAL g).|,x))) = 0 by Th1;
hence (Integral2 (L-Meas,|.(R_EAL g).|)) . x = 0 by MESFUN12:def 8; :: thesis:

end;

A9: for x, y being Element of REAL st x in I & y in J holds
( (ProjPMap1 (|.(R_EAL g).|,x)) . y = |.(R_EAL g).| . (x,y) & |.(R_EAL g).| . (x,y) = |.(g . [x,y]).| & |.(R_EAL g).| . (x,y) = |.g.| . [x,y] )

proof

end;

A13: for x being Element of REAL st x in I holds
0 <= (Integral2 (L-Meas,|.(R_EAL g).|)) . x

proof

let x be Element of REAL ; :: thesis:
assume A14: x in I ; :: thesis:
reconsider CD = J as Element of L-Field by MEASUR10:5, MEASUR12:75;
reconsider Pg = ProjPMap1 (|.(R_EAL g).|,x) as PartFunc of REAL,REAL by Th30;
A15: dom Pg = J by A14, A1, A3, Th27;
A16: Pg is CD -measurable by A14, A1, A2, A3, Th45;
A17: ( integral (Pg,J) = Integral (L-Meas,Pg) & integral (Pg,J) = (Integral2 (L-Meas,|.(R_EAL g).|)) . x ) by A14, A1, A2, A3, Th46;
for y being object st y in dom (Pg | J) holds
0 <= (Pg | J) . y

proof

end;

hence 0 <= (Integral2 (L-Meas,|.(R_EAL g).|)) . x by A15, A16, A17, MESFUNC6:52, MESFUNC6:84; :: thesis:

end;

proof

let r be Element of REAL ; :: thesis:
( r in I or r in H \ I ) by A25, XBOOLE_0:def 3;
hence 0 <= (Integral2 (L-Meas,|.(R_EAL g).|)) . r by A13, A8; :: thesis:

end;

then A29: Integral2 (L-Meas,|.(R_EAL g).|) is nonnegative ;
for r being Real holds H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) in L-Field

proof

per cases ;

suppose A31: r <= 0 ; :: thesis:

less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) = {}

proof

assume less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) <> {} ; :: thesis:
then consider x being object such that
A32: x in less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r) by XBOOLE_0:def 1;
( x in dom (Integral2 (L-Meas,|.(R_EAL g).|)) & (Integral2 (L-Meas,|.(R_EAL g).|)) . x < r ) by MESFUNC1:def 11, A32;
hence contradiction by A28, A31; :: thesis:

end;

hence H /\ (less_dom ((Integral2 (L-Meas,|.(R_EAL g).|)),r)) in L-Field by PROB_1:4; :: thesis:

end;

suppose A33: 0 < r ; :: thesis:

proof

let z be object ; :: thesis:

hereby :: thesis:

per cases by A34, A25, XBOOLE_0:def 3;

suppose A36: z in I ; :: thesis:

end;

suppose z in H \ I ; :: thesis:

hence z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | I),r)) \/ (H \ I) by XBOOLE_0:def 3; :: thesis:

end;

assume z in (less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | I),r)) \/ (H \ I) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose A37: z in less_dom (((Integral2 (L-Meas,|.(R_EAL g).|)) | I),r) ; :: thesis:

end;

suppose A39: z in H \ I ; :: thesis:

end;

end;

proof

end;

proof

let x be Element of REAL ; :: thesis:

per cases by A25, XBOOLE_0:def 3;

suppose A48: x in I ; :: thesis:

end;

suppose x in H \ I ; :: thesis:

then (Integral2 (L-Meas,|.(R_EAL g).|)) . x = 0 by A8;
hence (Integral2 (L-Meas,|.(R_EAL g).|)) . x < +infty by XREAL_0:def 1, XXREAL_0:9; :: thesis:

end;

hence ( g is_integrable_on Prod_Measure (L-Meas,L-Meas) & ( for x being Element of REAL holds (Integral2 (L-Meas,|.(R_EAL g).|)) . x < +infty ) & ( for U being Element of L-Field holds Integral2 (L-Meas,(R_EAL g)) is U -measurable ) & Integral2 (L-Meas,(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure (L-Meas,L-Meas)),g) = Integral (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) ) by A47, Th5, MESFUN13:32; :: thesis: