theorem :: MEASURE6:71

for X being set
for A being without_zero Subset of REAL
for f being Function of X,REAL holds (Inv f) " A = f " (Inv A)