theorem Th16: :: MEASUR14:16

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for A being Element of S
for B being Element of CopyField (T,S) st T is bijective & g = f * (T ") holds
for r being Real holds T .: (less_dom (f,r)) = less_dom (g,r)