theorem Th18: :: MESFUNC7:18

for X being non empty set
for f being PartFunc of X,ExtREAL
for A being set holds |.f.| | A = |.(f | A).|