theorem Th17: :: MEASUR14:17

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y st T is bijective holds
ex H being Function of Y,X st
( H is bijective & H = T " & H " = T & .: H = (.: T) " & (.: H) .: (CopyField (T,S)) = S & CopyField (H,(CopyField (T,S))) = S )