let I, J be non empty closed_interval Subset of REAL; :: thesis: for K being Subset of REAL
for v 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 = g & not v in [:I,J:] holds
( (Integral2 (L-Meas,|.(R_EAL g).|)) . v = 0 & (Integral2 (L-Meas,(R_EAL g))) . v = 0 )
let K be Subset of REAL; :: thesis: for v 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 = g & not v in [:I,J:] holds
( (Integral2 (L-Meas,|.(R_EAL g).|)) . v = 0 & (Integral2 (L-Meas,(R_EAL g))) . v = 0 )
let v 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 = g & not v in [:I,J:] holds
( (Integral2 (L-Meas,|.(R_EAL g).|)) . v = 0 & (Integral2 (L-Meas,(R_EAL g))) . v = 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 v in [:I,J:] holds
( (Integral2 (L-Meas,|.(R_EAL g).|)) . v = 0 & (Integral2 (L-Meas,(R_EAL g))) . v = 0 )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: ( [:[:I,J:],K:] = dom f & f = g & not v in [:I,J:] implies ( (Integral2 (L-Meas,|.(R_EAL g).|)) . v = 0 & (Integral2 (L-Meas,(R_EAL g))) . v = 0 ) )
assume that
A1: [:[:I,J:],K:] = dom f and
A2: f = g and
A3: not v in [:I,J:] ; :: thesis: ( (Integral2 (L-Meas,|.(R_EAL g).|)) . v = 0 & (Integral2 (L-Meas,(R_EAL g))) . v = 0 )
dom (ProjPMap1 (|.(R_EAL g).|,v)) = {} by A1, A2, A3, MESFUN16:27;
then Integral (L-Meas,(ProjPMap1 (|.(R_EAL g).|,v))) = 0 by MESFUN16:1;
hence (Integral2 (L-Meas,|.(R_EAL g).|)) . v = 0 by MESFUN12:def 8; :: thesis: (Integral2 (L-Meas,(R_EAL g))) . v = 0
dom (ProjPMap1 ((R_EAL g),v)) = {} by A1, A2, A3, MESFUN16:27;
then Integral (L-Meas,(ProjPMap1 ((R_EAL g),v))) = 0 by MESFUN16:1;
hence (Integral2 (L-Meas,(R_EAL g))) . v = 0 by MESFUN12:def 8; :: thesis: verum