theorem Th21: :: MEASUR14:21

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 st T is bijective holds
((.: T) | S) * F is Finite_Sep_Sequence of CopyField (T,S)