let I be Subset of REAL; :: thesis: for J being closed_interval Subset of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( (Integral2 (L-Meas,|.(R_EAL g).|)) | I is PartFunc of REAL,REAL & (Integral2 (L-Meas,(R_EAL g))) | I is PartFunc of REAL,REAL )
let J be closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( (Integral2 (L-Meas,|.(R_EAL g).|)) | I is PartFunc of REAL,REAL & (Integral2 (L-Meas,(R_EAL g))) | I is PartFunc of REAL,REAL )
let f be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:REAL,REAL:],REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( (Integral2 (L-Meas,|.(R_EAL g).|)) | I is PartFunc of REAL,REAL & (Integral2 (L-Meas,(R_EAL g))) | I is PartFunc of REAL,REAL )
let g be PartFunc of [:REAL,REAL:],REAL; :: thesis: ( [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g implies ( (Integral2 (L-Meas,|.(R_EAL g).|)) | I is PartFunc of REAL,REAL & (Integral2 (L-Meas,(R_EAL g))) | I is PartFunc of REAL,REAL ) )
assume that
A1: [:I,J:] = dom f and
A2: f is_continuous_on [:I,J:] and
A3: f = g ; :: thesis: ( (Integral2 (L-Meas,|.(R_EAL g).|)) | I is PartFunc of REAL,REAL & (Integral2 (L-Meas,(R_EAL g))) | I is PartFunc of REAL,REAL )

per cases ( not J is empty or J is empty ) ;

suppose not J is empty ; :: thesis: ( (Integral2 (L-Meas,|.(R_EAL g).|)) | I is PartFunc of REAL,REAL & (Integral2 (L-Meas,(R_EAL g))) | I is PartFunc of REAL,REAL )

then reconsider J1 = J as non empty closed_interval Subset of REAL ;
( [:I,J1:] = dom f & f is_continuous_on [:I,J1:] ) by A1, A2;
hence ( (Integral2 (L-Meas,|.(R_EAL g).|)) | I is PartFunc of REAL,REAL & (Integral2 (L-Meas,(R_EAL g))) | I is PartFunc of REAL,REAL ) by A3, MESFUN16:51; :: thesis: verum

end;

suppose J is empty ; :: thesis: ( (Integral2 (L-Meas,|.(R_EAL g).|)) | I is PartFunc of REAL,REAL & (Integral2 (L-Meas,(R_EAL g))) | I is PartFunc of REAL,REAL )

hence ( (Integral2 (L-Meas,|.(R_EAL g).|)) | I is PartFunc of REAL,REAL & (Integral2 (L-Meas,(R_EAL g))) | I is PartFunc of REAL,REAL ) by A1, A3, Lm1; :: thesis: verum

end;

end;