:: deftheorem defines CopyMeasure MEASUR14:def 3 :
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
for b₆ being Measure of (CopyField (f,S)) holds
( b₆ = CopyMeasure (f,M) iff ( b₆ = M * (((.: f) | S) ") & ( for s being Element of CopyField (f,S) ex t being Element of S st
( s = f .: t & b₆ . s = M . t ) ) ) );