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
for x being Element of REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is Function of REAL,REAL & ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is Function of 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
for x being Element of REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is Function of REAL,REAL & ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is Function of REAL,REAL )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for x being Element of REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is Function of REAL,REAL & ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is Function of REAL,REAL )
let x be Element of REAL ; :: thesis: ( [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g implies ( ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is Function of REAL,REAL & ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is Function of REAL,REAL ) )
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f is_continuous_on [:[:I,J:],K:] and
A3: f = g ; :: thesis: ( ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is Function of REAL,REAL & ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is Function of REAL,REAL )
reconsider F2 = Integral2 (L-Meas,(R_EAL g)) as Function of [:REAL,REAL:],REAL by A1, A2, A3, Th32;
A4: dom (Integral2 (L-Meas,(R_EAL g))) = [:REAL,REAL:] by FUNCT_2:def 1;
then A5: dom |.(Integral2 (L-Meas,(R_EAL g))).| = [:REAL,REAL:] by MESFUNC1:def 10;
dom F2 = [:REAL,REAL:] by FUNCT_2:def 1;
then A6: dom |.F2.| = [:REAL,REAL:] by VALUED_1:def 11;
A7: [#] REAL = REAL by SUBSET_1:def 3;
then A8: dom (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) = REAL by A4, MESFUN16:25;
A9: dom (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) = REAL by A7, A5, MESFUN16:25;
A10: dom (ProjPMap1 (F2,x)) = REAL by A7, A4, MESFUN16:25;
A11: dom (ProjPMap1 (|.F2.|,x)) = REAL by A6, A7, MESFUN16:25;

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

let r be object ; :: thesis: ( r in rng (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) implies r in REAL )
assume r in rng (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) ; :: thesis: r in REAL
then consider y being Element of REAL such that
A12: ( y in dom (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) & r = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) . y ) by PARTFUN1:3;
A13: [x,y] in [:REAL,REAL:] ;
then [x,y] in dom (Integral2 (L-Meas,(R_EAL g))) by FUNCT_2:def 1;
then A14: r = F2 . (x,y) by A12, MESFUN12:def 3;
[x,y] in dom F2 by A13, FUNCT_2:def 1;
then r = (ProjPMap1 (F2,x)) . y by A14, MESFUN12:def 3;
then r in rng (ProjPMap1 (F2,x)) by A10, FUNCT_1:3;
hence r in REAL ; :: thesis: verum

end;

then rng (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) c= REAL ;
hence ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is Function of REAL,REAL by A8, FUNCT_2:2; :: thesis: ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is Function of REAL,REAL

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

let r be object ; :: thesis: ( r in rng (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) implies r in REAL )
assume r in rng (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) ; :: thesis: r in REAL
then consider y being Element of REAL such that
A15: ( y in dom (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) & r = (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) . y ) by PARTFUN1:3;
[x,y] in [:REAL,REAL:] ;
then A16: [x,y] in dom (Integral2 (L-Meas,(R_EAL g))) by FUNCT_2:def 1;
then A17: [x,y] in dom |.(Integral2 (L-Meas,(R_EAL g))).| by MESFUNC1:def 10;
then r = |.(Integral2 (L-Meas,(R_EAL g))).| . (x,y) by A15, MESFUN12:def 3;
then A18: r = |.((Integral2 (L-Meas,(R_EAL g))) . (x,y)).| by A17, MESFUNC1:def 10;
set p = [x,y];
reconsider p = [x,y] as Element of [:REAL,REAL:] ;
A19: p in dom |.F2.| by A16, VALUED_1:def 11;
r = |.(F2 . p).| by A18, EXTREAL1:12;
then r = |.F2.| . (x,y) by A19, VALUED_1:def 11;
then r = (ProjPMap1 (|.F2.|,x)) . y by A19, MESFUN12:def 3;
then r in rng (ProjPMap1 (|.F2.|,x)) by A11, FUNCT_1:3;
hence r in REAL ; :: thesis: verum

end;

then rng (ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x)) c= REAL ;
hence ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is Function of REAL,REAL by A9, FUNCT_2:2; :: thesis: verum