:: deftheorem Def4 defines CopyMeasure MEASUR14:def 4 :
for X, Y being non empty set
for f being Function of X,Y
for S being SigmaField of X
for M being sigma_Measure of S st f is bijective holds
for b₆ being sigma_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 ) ) ) );