let I, J be non empty closed_interval Subset of REAL; :: thesis: for K being Subset of REAL
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
for Pg2 being PartFunc of [:REAL,REAL:],REAL st z in K & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,z) holds
( Pg2 is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 (|.(R_EAL g).|,z))) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z )
let K be 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
for Pg2 being PartFunc of [:REAL,REAL:],REAL st z in K & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,z) holds
( Pg2 is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 (|.(R_EAL g).|,z))) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z )
let z 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
for Pg2 being PartFunc of [:REAL,REAL:],REAL st z in K & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,z) holds
( Pg2 is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 (|.(R_EAL g).|,z))) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z )
let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pg2 being PartFunc of [:REAL,REAL:],REAL st z in K & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,z) holds
( Pg2 is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 (|.(R_EAL g).|,z))) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for Pg2 being PartFunc of [:REAL,REAL:],REAL st z in K & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,z) holds
( Pg2 is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 (|.(R_EAL g).|,z))) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z )
let Pg2 be PartFunc of [:REAL,REAL:],REAL; :: thesis: ( z in K & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,z) implies ( Pg2 is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 (|.(R_EAL g).|,z))) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z ) )
assume that
A1: z in K and
A2: dom f = [:[:I,J:],K:] and
A3: f is_continuous_on [:[:I,J:],K:] and
A4: f = g and
A5: Pg2 = ProjPMap2 (|.(R_EAL g).|,z) ; :: thesis: ( Pg2 is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 (|.(R_EAL g).|,z))) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z )
reconsider Pf2 = Pg2 as PartFunc of [:RNS_Real,RNS_Real:],RNS_Real ;
A6: dom Pf2 = [:I,J:] by A1, A2, A4, A5, MESFUN16:28;
then Pf2 is_continuous_on [:I,J:] by A2, A3, A4, A5, Th20;
hence Pg2 is_integrable_on Prod_Measure (L-Meas,L-Meas) by A6, MESFUN16:57; :: thesis: ( Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 (|.(R_EAL g).|,z))) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z )
thus Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 (|.(R_EAL g).|,z))) by A5, MESFUNC5:def 7; :: thesis: Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z
R_EAL Pg2 = ProjPMap2 (|.(R_EAL g).|,z) by A5, MESFUNC5:def 7;
hence Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z by MESFUN12:def 7; :: thesis: verum