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 y being Element of REAL st y in REAL \ J holds
(Integral1 (L-Meas,|.(R_EAL g).|)) . y = 0

proof

let y be Element of REAL ; :: thesis:
assume y in REAL \ J ; :: thesis:
then not y in J by XBOOLE_0:def 5;
then A9: dom (ProjPMap2 (|.(R_EAL g).|,y)) = {} by A1, A3, Th28;
(Integral1 (L-Meas,|.(R_EAL g).|)) . y = Integral (L-Meas,(ProjPMap2 (|.(R_EAL g).|,y))) by MESFUN12:def 7;
hence (Integral1 (L-Meas,|.(R_EAL g).|)) . y = 0 by A9, Th1; :: thesis:

end;

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

proof

end;

A15: for y being Element of REAL st y in J holds
0 <= (Integral1 (L-Meas,|.(R_EAL g).|)) . y

proof

let y be Element of REAL ; :: thesis:
assume A16: y in J ; :: thesis:
reconsider AB = I as Element of L-Field by MEASUR10:5, MEASUR12:75;
reconsider Pg = ProjPMap2 (|.(R_EAL g).|,y) as PartFunc of REAL,REAL by Th30;
A17: dom Pg = I by A16, A1, A3, Th28;
A18: Pg is AB -measurable by A16, A1, A2, A3, Th48;
A19: ( integral (Pg,I) = Integral (L-Meas,Pg) & integral (Pg,I) = (Integral1 (L-Meas,|.(R_EAL g).|)) . y ) by A16, A1, A2, A3, Th49;
for x being object st x in dom (Pg | I) holds
0 <= (Pg | I) . x

proof

end;

hence 0 <= (Integral1 (L-Meas,|.(R_EAL g).|)) . y by A17, A18, A19, MESFUNC6:52, MESFUNC6:84; :: thesis:

end;

proof

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

end;

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

proof

per cases ;

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

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

proof

assume less_dom ((Integral1 (L-Meas,|.(R_EAL g).|)),r) <> {} ; :: thesis:
then consider y being object such that
A34: y in less_dom ((Integral1 (L-Meas,|.(R_EAL g).|)),r) by XBOOLE_0:def 1;
( y in dom (Integral1 (L-Meas,|.(R_EAL g).|)) & (Integral1 (L-Meas,|.(R_EAL g).|)) . y < r ) by MESFUNC1:def 11, A34;
hence contradiction by A30, A33; :: thesis:

end;

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

end;

suppose A35: 0 < r ; :: thesis:

proof

let z be object ; :: thesis:

hereby :: thesis:

per cases by A36, A27, XBOOLE_0:def 3;

suppose A38: z in J ; :: thesis:

end;

suppose z in H \ J ; :: thesis:

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

end;

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

per cases by XBOOLE_0:def 3;

suppose A39: z in less_dom (((Integral1 (L-Meas,|.(R_EAL g).|)) | J),r) ; :: thesis:

end;

suppose A41: z in H \ J ; :: thesis:

end;

end;

proof

end;

proof

let y be Element of REAL ; :: thesis:

per cases by A27, XBOOLE_0:def 3;

suppose A50: y in J ; :: thesis:

end;

suppose y in H \ J ; :: thesis:

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

end;

hence ( g is_integrable_on Prod_Measure (L-Meas,L-Meas) & ( for y being Element of REAL holds (Integral1 (L-Meas,|.(R_EAL g).|)) . y < +infty ) & ( for V being Element of L-Field holds Integral1 (L-Meas,(R_EAL g)) is V -measurable ) & Integral1 (L-Meas,(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure (L-Meas,L-Meas)),g) = Integral (L-Meas,(Integral1 (L-Meas,(R_EAL g)))) ) by A49, Th5, MESFUN13:33; :: thesis: