let I, J, K be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( Integral2 (L-Meas,|.(R_EAL g).|) is Function of [:REAL,REAL:],REAL & (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL & Integral2 (L-Meas,(R_EAL g)) is Function of [:REAL,REAL:],REAL & (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL )
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( Integral2 (L-Meas,|.(R_EAL g).|) is Function of [:REAL,REAL:],REAL & (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL & Integral2 (L-Meas,(R_EAL g)) is Function of [:REAL,REAL:],REAL & (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: ( [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g implies ( Integral2 (L-Meas,|.(R_EAL g).|) is Function of [:REAL,REAL:],REAL & (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL & Integral2 (L-Meas,(R_EAL g)) is Function of [:REAL,REAL:],REAL & (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL ) )
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f is_continuous_on [:[:I,J:],K:] and
A3: f = g ; :: thesis: ( Integral2 (L-Meas,|.(R_EAL g).|) is Function of [:REAL,REAL:],REAL & (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL & Integral2 (L-Meas,(R_EAL g)) is Function of [:REAL,REAL:],REAL & (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL )
set F = Integral2 (L-Meas,|.(R_EAL g).|);
set RF = Integral2 (L-Meas,(R_EAL g));
A4: dom (Integral2 (L-Meas,|.(R_EAL g).|)) = [:REAL,REAL:] by FUNCT_2:def 1;
A5: dom (Integral2 (L-Meas,(R_EAL g))) = [:REAL,REAL:] by FUNCT_2:def 1;

now :: thesis: for q being object st q in rng (Integral2 (L-Meas,|.(R_EAL g).|)) holds
q in REAL

let q be object ; :: thesis: ( q in rng (Integral2 (L-Meas,|.(R_EAL g).|)) implies b₁ in REAL )
assume q in rng (Integral2 (L-Meas,|.(R_EAL g).|)) ; :: thesis: b₁ in REAL
then consider p being Element of [:REAL,REAL:] such that
A6: ( p in dom (Integral2 (L-Meas,|.(R_EAL g).|)) & q = (Integral2 (L-Meas,|.(R_EAL g).|)) . p ) by PARTFUN1:3;
consider x, y being object such that
A7: ( x in REAL & y in REAL & p = [x,y] ) by ZFMISC_1:84;
reconsider x = x, y = y as Element of REAL by A7;
reconsider Pg = ProjPMap1 (|.(R_EAL g).|,[x,y]) as PartFunc of REAL,REAL by MESFUN16:30;

per cases ( p in [:I,J:] or not p in [:I,J:] ) ;

suppose p in [:I,J:] ; :: thesis: b₁ in REAL

then ( x in I & y in J ) by A7, ZFMISC_1:87;
then (Integral2 (L-Meas,|.(R_EAL g).|)) . [x,y] = integral (Pg,K) by A1, A2, A3, Th26;
hence q in REAL by A6, A7, XREAL_0:def 1; :: thesis: verum

end;

suppose not p in [:I,J:] ; :: thesis: b₁ in REAL

then (Integral2 (L-Meas,|.(R_EAL g).|)) . p = 0 by A1, A3, Lm4;
hence q in REAL by A6, XREAL_0:def 1; :: thesis: verum

end;

end;

end;

then rng (Integral2 (L-Meas,|.(R_EAL g).|)) c= REAL ;
hence Integral2 (L-Meas,|.(R_EAL g).|) is Function of [:REAL,REAL:],REAL by A4, RELSET_1:4; :: thesis: ( (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL & Integral2 (L-Meas,(R_EAL g)) is Function of [:REAL,REAL:],REAL & (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL )
hence (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL by PARTFUN1:11; :: thesis: ( Integral2 (L-Meas,(R_EAL g)) is Function of [:REAL,REAL:],REAL & (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL )

now :: thesis: for q being object st q in rng (Integral2 (L-Meas,(R_EAL g))) holds
q in REAL

let q be object ; :: thesis: ( q in rng (Integral2 (L-Meas,(R_EAL g))) implies b₁ in REAL )
assume q in rng (Integral2 (L-Meas,(R_EAL g))) ; :: thesis: b₁ in REAL
then consider p being Element of [:REAL,REAL:] such that
A8: ( p in dom (Integral2 (L-Meas,(R_EAL g))) & q = (Integral2 (L-Meas,(R_EAL g))) . p ) by PARTFUN1:3;
consider x, y being object such that
A9: ( x in REAL & y in REAL & p = [x,y] ) by ZFMISC_1:84;
reconsider x = x, y = y as Element of REAL by A9;
reconsider Pg = ProjPMap1 ((R_EAL g),[x,y]) as PartFunc of REAL,REAL by MESFUN16:30;

per cases ( p in [:I,J:] or not p in [:I,J:] ) ;

suppose p in [:I,J:] ; :: thesis: b₁ in REAL

then ( x in I & y in J ) by A9, ZFMISC_1:87;
then (Integral2 (L-Meas,(R_EAL g))) . [x,y] = integral (Pg,K) by A1, A2, A3, Th22;
hence q in REAL by A8, A9, XREAL_0:def 1; :: thesis: verum

end;

suppose not p in [:I,J:] ; :: thesis: b₁ in REAL

then (Integral2 (L-Meas,(R_EAL g))) . p = 0 by A1, A3, Lm4;
hence q in REAL by A8, XREAL_0:def 1; :: thesis: verum

end;

end;

end;

then rng (Integral2 (L-Meas,(R_EAL g))) c= REAL ;
hence Integral2 (L-Meas,(R_EAL g)) is Function of [:REAL,REAL:],REAL by A5, RELSET_1:4; :: thesis: (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL
hence (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL by PARTFUN1:11; :: thesis: verum