theorem Th24: :: MEASUR14:24

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") & F,a are_Re-presentation_of f holds
ex G being Finite_Sep_Sequence of CopyField (T,S) st
( G = ((.: T) | S) * F & G,a are_Re-presentation_of g )