:: deftheorem Def7 defines Integral1 MESFUN12:def 7 :
for X1, X2 being non empty set
for S1 being SigmaField of X1
for M1 being sigma_Measure of S1
for f being PartFunc of [:X1,X2:],ExtREAL
for b₆ being Function of X2,ExtREAL holds
( b₆ = Integral1 (M1,f) iff for y being Element of X2 holds b₆ . y = Integral (M1,(ProjPMap2 (f,y))) );