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

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

suppose A5: u in [:I,J:] ; :: thesis: (Integral2 (L-Meas,|.(R_EAL g).|)) . u < +infty

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

end;

suppose not u in [:I,J:] ; :: thesis: (Integral2 (L-Meas,|.(R_EAL g).|)) . u < +infty

then (Integral2 (L-Meas,|.(R_EAL g).|)) . u = 0 by A1, A3, Lm4;
hence (Integral2 (L-Meas,|.(R_EAL g).|)) . u < +infty by XREAL_0:def 1, XXREAL_0:9; :: thesis: verum

end;

end;