:: deftheorem Def2 defines CopyField MEASUR14:def 2 :
for X, Y being non empty set
for f being Function of X,Y
for S being SigmaField of X st f is bijective holds
CopyField (f,S) = (.: f) .: S;