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 E being Element of L-Field 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 E -measurable
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for E being Element of L-Field 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 E -measurable
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for E being Element of L-Field 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 E -measurable
let E be Element of L-Field ; :: 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 E -measurable )
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 E -measurable
set F = Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|);
set F0 = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K;
A4: 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).|)) | 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;
reconsider GG = G as PartFunc of RNS_Real,RNS_Real ;
A6: K is Element of L-Field by MEASUR10:5, MEASUR12:75;
( G | K is bounded & G is_integrable_on K ) by A1, A2, A3, A5, Th36, INTEGRA5:10, INTEGRA5:11;
then G is_integrable_on L-Meas by A5, A6, MESFUN14:49;
then A7: (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K is_integrable_on L-Meas by MESFUNC5:def 7;
reconsider R = REAL as Element of L-Field by PROB_1:5;
set NK = R \ K;
A8: R \ K is Element of L-Field by A6, PROB_1:6;
A9: K \/ (R \ K) = REAL by XBOOLE_1:45;
A10: K /\ (R \ K) = {} by XBOOLE_1:85, XBOOLE_0:def 7;
A11: Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|) is nonnegative by A1, A2, A3, Th39;
for r being Real holds R /\ (less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r)) in L-Field

proof

let r be Real; :: thesis: R /\ (less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r)) in L-Field
A12: ex E being Element of L-Field st
( E = dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K) & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K is E -measurable ) by A7, MESFUNC5:def 17;

per cases ( r <= 0 or 0 < r ) ;

suppose A13: r <= 0 ; :: thesis: R /\ (less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r)) in L-Field

less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r) = {}

proof

assume less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r) <> {} ; :: thesis: contradiction
then consider x being object such that
A14: x in less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r) by XBOOLE_0:def 1;
( x in dom (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . x < r ) by A14, MESFUNC1:def 11;
hence contradiction by A11, A13; :: thesis: verum

end;

hence R /\ (less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r)) in L-Field by PROB_1:4; :: thesis: verum

end;

suppose A15: 0 < r ; :: thesis: R /\ (less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r)) in L-Field

for z being object holds
( z in less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r) iff z in (less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K) )

proof

let z be object ; :: thesis: ( z in less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r) iff z in (less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K) )

hereby :: thesis: ( z in (less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K) implies z in less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r) )

assume A16: z in less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r) ; :: thesis: z in (less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K)
then A17: (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z < r by MESFUNC1:def 11;
A18: ( z in R \ K implies z in (less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K) ) by XBOOLE_0:def 3;

now :: thesis: ( z in K implies z in (less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K) )

assume A19: z in K ; :: thesis: z in (less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K)
then ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K) . z < r by A17, FUNCT_1:49;
then z in less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r) by A5, A19, MESFUNC1:def 11;
hence z in (less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K) by XBOOLE_0:def 3; :: thesis: verum

end;

hence z in (less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K) by A9, A16, A18, XBOOLE_0:def 3; :: thesis: verum

end;

assume z in (less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K) ; :: thesis: z in less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r)

per cases then ( z in less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r) or z in R \ K ) by XBOOLE_0:def 3;

suppose A20: z in less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r) ; :: thesis: z in less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r)

then ( z in dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K) & ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K) . z < r ) by MESFUNC1:def 11;
then (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z < r by FUNCT_1:49;
hence z in less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r) by A4, A20, MESFUNC1:def 11; :: thesis: verum

end;

suppose A21: z in R \ K ; :: thesis: z in less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r)

then not z in K by XBOOLE_0:def 5;
then (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z < r by A15, A1, A3, A21, Lm5;
hence z in less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r) by A4, A21, MESFUNC1:def 11; :: thesis: verum

end;

end;

end;

then less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r) = (less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K) by TARSKI:2;
then A22: R /\ (less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r)) = (K /\ ((less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K))) \/ ((R \ K) /\ ((less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K))) by A9, XBOOLE_1:23;
K /\ ((less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K)) = (K /\ (less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r))) \/ (K /\ (R \ K)) by XBOOLE_1:23;
then A23: K /\ ((less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K)) in L-Field by A4, A10, A12;
A24: less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r) c= K by A5, MESFUNC1:def 11;
(R \ K) /\ ((less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K)) = ((R \ K) /\ (less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r))) \/ ((R \ K) /\ (R \ K)) by XBOOLE_1:23;
then (R \ K) /\ ((less_dom (((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K),r)) \/ (R \ K)) = {} \/ ((R \ K) /\ (R \ K)) by A24;
hence R /\ (less_dom ((Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)),r)) in L-Field by A8, A22, A23, PROB_1:3; :: thesis: verum

end;

end;

end;

then Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|) is R -measurable ;
hence Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|) is E -measurable by MESFUNC1:30; :: thesis: verum