theorem Th5: :: MEASUR14:5

for X, Y being non empty set
for f being Function of X,Y
for S being Field_Subset of X
for M being Measure of S st f is bijective holds
ex M1 being Measure of (CopyField (f,S)) st
( M1 = M * (((.: f) | S) ") & ( for s being Element of CopyField (f,S) ex t being Element of S st
( s = f .: t & M1 . s = M . t ) ) )