let I, J be Subset of REAL; :: thesis: for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st J is empty & [:I,J:] = dom f & 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 J is empty & [:I,J:] = dom f & 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: ( J is empty & [:I,J:] = dom f & 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: J is empty and
A2: [:I,J:] = dom f 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 by PARTFUN1:11;
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 MESFUN16:30;
A6: (Integral2 (L-Meas,|.(R_EAL g).|)) . x = Integral (L-Meas,(ProjPMap1 (|.(R_EAL g).|,x))) by MESFUN12:def 8;
x in (dom (Integral2 (L-Meas,|.(R_EAL g).|))) /\ I by A5, RELAT_1:61;
then x in I by XBOOLE_0:def 4;
then dom (ProjPMap1 (|.(R_EAL g).|,x)) = J by A2, A3, MESFUN16:27;
then (Integral2 (L-Meas,|.(R_EAL g).|)) . x = 0 by A1, A6, MESFUN16:1;
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 by PARTFUN1:11;
A7: 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
A8: ( x in dom GI & y = GI . x ) by PARTFUN1:3;
reconsider Pg = ProjPMap1 ((R_EAL g),x) as PartFunc of REAL,REAL by MESFUN16:30;
A9: (Integral2 (L-Meas,(R_EAL g))) . x = Integral (L-Meas,(ProjPMap1 ((R_EAL g),x))) by MESFUN12:def 8;
x in (dom (Integral2 (L-Meas,(R_EAL g)))) /\ I by A8, RELAT_1:61;
then x in I by XBOOLE_0:def 4;
then dom (ProjPMap1 ((R_EAL g),x)) = J by A2, A3, MESFUN16:27;
then (Integral2 (L-Meas,(R_EAL g))) . x = 0 by A1, A9, MESFUN16:1;
then (Integral2 (L-Meas,(R_EAL g))) . x in REAL by XREAL_0:def 1;
hence y in REAL by A8, A7, 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