let I be Subset of REAL; :: thesis: for J being non empty 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 non empty 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 )
set Rg = R_EAL g;
set F = Integral2 (L-Meas,|.(R_EAL g).|);
reconsider FI = (Integral2 (L-Meas,|.(R_EAL g).|)) | I as PartFunc of REAL,ExtREAL ;
A4: dom (Integral2 (L-Meas,|.(R_EAL g).|)) = REAL by FUNCT_2:def 1;

now :: thesis: for y being object st y in rng FI holds
y in REAL

let y be object ; :: thesis: ( y in rng FI implies y in REAL )
assume y in rng FI ; :: thesis: y in REAL
then consider x being Element of REAL such that
A5: ( x in dom FI & y = FI . x ) by PARTFUN1:3;
reconsider Pg = ProjPMap1 (|.(R_EAL g).|,x) as PartFunc of REAL,REAL by Th30;
(Integral2 (L-Meas,|.(R_EAL g).|)) . x = integral (Pg,J) by A5, A4, A1, A2, A3, Th46;
then (Integral2 (L-Meas,|.(R_EAL g).|)) . x in REAL by XREAL_0:def 1;
hence y in REAL by A5, A4, FUNCT_1:49; :: thesis: verum

end;

then ( rng FI c= REAL & dom FI c= REAL ) ;
hence (Integral2 (L-Meas,|.(R_EAL g).|)) | I is PartFunc of REAL,REAL by RELSET_1:4; :: thesis: (Integral2 (L-Meas,(R_EAL g))) | I is PartFunc of REAL,REAL
set G = Integral2 (L-Meas,(R_EAL g));
reconsider GI = (Integral2 (L-Meas,(R_EAL g))) | I as PartFunc of REAL,ExtREAL ;
A6: dom (Integral2 (L-Meas,(R_EAL g))) = REAL by FUNCT_2:def 1;

now :: thesis: for y being object st y in rng GI holds
y in REAL

let y be object ; :: thesis: ( y in rng GI implies y in REAL )
assume y in rng GI ; :: thesis: y in REAL
then consider x being Element of REAL such that
A7: ( x in dom GI & y = GI . x ) by PARTFUN1:3;
reconsider Pg = ProjPMap1 ((R_EAL g),x) as PartFunc of REAL,REAL by Th30;
(Integral2 (L-Meas,(R_EAL g))) . x = integral (Pg,J) by A7, A6, A1, A2, A3, Th41;
then (Integral2 (L-Meas,(R_EAL g))) . x in REAL by XREAL_0:def 1;
hence y in REAL by A7, A6, FUNCT_1:49; :: thesis: verum

end;

then ( rng GI c= REAL & dom GI c= REAL ) ;
hence (Integral2 (L-Meas,(R_EAL g))) | I is PartFunc of REAL,REAL by RELSET_1:4; :: thesis: verum