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
|.(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))).| 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 st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
|.(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))).| is Function of 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 |.(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))).| 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: |.(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))).| is Function of REAL,REAL
set Fxy = Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g));
A4: Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is Function of REAL,REAL by A1, A2, A3, Th35;
dom (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) = REAL by FUNCT_2:def 1;
then A5: dom |.(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))).| = REAL by MESFUNC1:def 10;

now :: thesis: for r being object st r in REAL holds
|.(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))).| . r in REAL

let r be object ; :: thesis: ( r in REAL implies |.(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))).| . r in REAL )
assume r in REAL ; :: thesis: |.(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))).| . r in REAL
then reconsider r1 = r as Element of REAL ;
A6: |.(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))).| . r = |.((Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . r1).| by A5, MESFUNC1:def 10;
reconsider y = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . r1 as Element of REAL by A4, FUNCT_2:5;
|.(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))).| . r = |.y.| by A6, EXTREAL1:12;
hence |.(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))).| . r in REAL by XREAL_0:def 1; :: thesis: verum

end;

hence |.(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))).| is Function of REAL,REAL by A5, FUNCT_2:3; :: thesis: verum