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 y being Element of REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) is Function of REAL,REAL & ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) 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 y being Element of REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) is Function of REAL,REAL & ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) is Function of REAL,REAL )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for y being Element of REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) is Function of REAL,REAL & ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) is Function of REAL,REAL )
let y be Element of REAL ; :: thesis: ( [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g implies ( ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) is Function of REAL,REAL & ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) 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: ( ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) is Function of REAL,REAL & ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) 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 (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) = REAL by A4, MESFUN16:26;
A9: dom (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) = REAL by A7, A5, MESFUN16:26;
A10: dom (ProjPMap2 (F2,y)) = REAL by A7, A4, MESFUN16:26;
A11: dom (ProjPMap2 (|.F2.|,y)) = REAL by A6, A7, MESFUN16:26;

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

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

end;

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

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

let r be object ; :: thesis: ( r in rng (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) implies r in REAL )
assume r in rng (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) ; :: thesis: r in REAL
then consider x being Element of REAL such that
A15: ( x in dom (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) & r = (ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y)) . x ) 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 4;
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 = (ProjPMap2 (|.F2.|,y)) . x by A19, MESFUN12:def 4;
then r in rng (ProjPMap2 (|.F2.|,y)) by A11, FUNCT_1:3;
hence r in REAL ; :: thesis: verum

end;

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