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 st [:[:I,J:],K:] = dom f & f = g & not z in K holds
( (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z = 0 & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z = 0 )
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 st [:[:I,J:],K:] = dom f & f = g & not z in K holds
( (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z = 0 & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z = 0 )
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 st [:[:I,J:],K:] = dom f & f = g & not z in K holds
( (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z = 0 & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z = 0 )
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 = g & not z in K holds
( (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z = 0 & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z = 0 )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: ( [:[:I,J:],K:] = dom f & f = g & not z in K implies ( (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z = 0 & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z = 0 ) )
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f = g and
A3: not z in K ; :: thesis: ( (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z = 0 & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z = 0 )
dom (ProjPMap2 (|.(R_EAL g).|,z)) = {} by A1, A2, A3, MESFUN16:28;
then Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 (|.(R_EAL g).|,z))) = 0 by MESFUN16:1;
hence (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z = 0 by MESFUN12:def 7; :: thesis: (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z = 0
dom (ProjPMap2 ((R_EAL g),z)) = {} by A1, A2, A3, MESFUN16:28;
then Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 ((R_EAL g),z))) = 0 by MESFUN16:1;
hence (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z = 0 by MESFUN12:def 7; :: thesis: verum