let I, J, K be non empty closed_interval Subset of REAL; :: thesis: for z being Element of REAL
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).|)) . z < +infty
let y be Element 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).|)) . y < +infty
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).|)) . y < +infty
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).|)) . y < +infty )
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).|)) . y < +infty
dom (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) = REAL by FUNCT_2:def 1;
then A4: dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K) = K ;
reconsider G = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K as PartFunc of REAL,REAL by A1, A2, A3, Th35;

per cases ( y in K or not y in K ) ;

suppose A5: y in K ; :: thesis: (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . y < +infty

then (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . y = G . y by FUNCT_1:49;
then (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . y in rng G by A4, A5, FUNCT_1:3;
hence (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . y < +infty by XXREAL_0:9; :: thesis: verum

end;

suppose not y in K ; :: thesis: (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . y < +infty

then dom (ProjPMap2 (|.(R_EAL g).|,y)) = {} by A1, A3, MESFUN16:28;
then Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 (|.(R_EAL g).|,y))) = 0 by MESFUN16:1;
then (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . y = 0 by MESFUN12:def 7;
hence (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . y < +infty by XREAL_0:def 1, XXREAL_0:9; :: thesis: verum

end;

end;