theorem Th4: :: MEASUR14:4

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 G being Function of S,(CopyField (f,S)) st
( G = (.: f) | S & dom G = S & rng G = CopyField (f,S) & G is bijective ) & ex F being Function of (CopyField (f,S)),S st
( F = ((.: f) | S) " & rng F = S & dom F = CopyField (f,S) & F is bijective ) )