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