let I, J be non empty closed_interval Subset of REAL; :: thesis: for g being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for f being PartFunc of [:REAL,REAL:],REAL st [:I,J:] = dom g & g is_continuous_on [:I,J:] & g = f holds
( (Integral1 (L-Meas,|.(R_EAL f).|)) | J is PartFunc of REAL,REAL & (Integral1 (L-Meas,(R_EAL f))) | J is PartFunc of REAL,REAL )
let g be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis: for f being PartFunc of [:REAL,REAL:],REAL st [:I,J:] = dom g & g is_continuous_on [:I,J:] & g = f holds
( (Integral1 (L-Meas,|.(R_EAL f).|)) | J is PartFunc of REAL,REAL & (Integral1 (L-Meas,(R_EAL f))) | J is PartFunc of REAL,REAL )
let f be PartFunc of [:REAL,REAL:],REAL; :: thesis: ( [:I,J:] = dom g & g is_continuous_on [:I,J:] & g = f implies ( (Integral1 (L-Meas,|.(R_EAL f).|)) | J is PartFunc of REAL,REAL & (Integral1 (L-Meas,(R_EAL f))) | J is PartFunc of REAL,REAL ) )
assume that
A1: [:I,J:] = dom g and
A2: g is_continuous_on [:I,J:] and
A3: g = f ; :: thesis: ( (Integral1 (L-Meas,|.(R_EAL f).|)) | J is PartFunc of REAL,REAL & (Integral1 (L-Meas,(R_EAL f))) | J is PartFunc of REAL,REAL )
set g1 = R_EAL f;
set T = Integral1 (L-Meas,|.(R_EAL f).|);
A4: dom (Integral1 (L-Meas,|.(R_EAL f).|)) = REAL by FUNCT_2:def 1;
reconsider T0 = (Integral1 (L-Meas,|.(R_EAL f).|)) | J as PartFunc of REAL,ExtREAL ;
set RT = Integral1 (L-Meas,(R_EAL f));
A5: dom (Integral1 (L-Meas,(R_EAL f))) = REAL by FUNCT_2:def 1;
reconsider RT0 = (Integral1 (L-Meas,(R_EAL f))) | J as PartFunc of REAL,ExtREAL ;

now :: thesis: for x being object st x in rng T0 holds
x in REAL

let x be object ; :: thesis: ( x in rng T0 implies x in REAL )
assume x in rng T0 ; :: thesis: x in REAL
then consider y being Element of REAL such that
A6: ( y in dom T0 & x = T0 . y ) by PARTFUN1:3;
reconsider Pg = ProjPMap2 (|.(R_EAL f).|,y) as PartFunc of REAL,REAL by Th30;
(Integral1 (L-Meas,|.(R_EAL f).|)) . y = integral (Pg,I) by A6, A4, A1, A2, A3, Th49;
then (Integral1 (L-Meas,|.(R_EAL f).|)) . y in REAL by XREAL_0:def 1;
hence x in REAL by A6, A4, FUNCT_1:49; :: thesis: verum

end;

then ( rng T0 c= REAL & dom T0 c= REAL ) ;
hence (Integral1 (L-Meas,|.(R_EAL f).|)) | J is PartFunc of REAL,REAL by RELSET_1:4; :: thesis: (Integral1 (L-Meas,(R_EAL f))) | J is PartFunc of REAL,REAL

now :: thesis: for x being object st x in rng RT0 holds
x in REAL

let x be object ; :: thesis: ( x in rng RT0 implies x in REAL )
assume x in rng RT0 ; :: thesis: x in REAL
then consider y being Element of REAL such that
A7: ( y in dom RT0 & x = RT0 . y ) by PARTFUN1:3;
reconsider Pg = ProjPMap2 ((R_EAL f),y) as PartFunc of REAL,REAL by Th30;
(Integral1 (L-Meas,(R_EAL f))) . y = integral (Pg,I) by A7, A5, A1, A2, A3, Th43;
then (Integral1 (L-Meas,(R_EAL f))) . y in REAL by XREAL_0:def 1;
hence x in REAL by A7, A5, FUNCT_1:49; :: thesis: verum

end;

then ( rng RT0 c= REAL & dom RT0 c= REAL ) ;
hence (Integral1 (L-Meas,(R_EAL f))) | J is PartFunc of REAL,REAL by RELSET_1:4; :: thesis: verum