for I1 being set
for I2, I3 being non empty set
for f being Function of I1,I2
for g being Function of I2,I3
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for C being ManySortedSet of I3
for F being MSUnTrans of f,A,B
for G being MSUnTrans of g * f,B * f,C st ( for ii being set st ii in I1 & (B * f) . ii = {} & not A . ii = {} holds
(C * (g * f)) . ii = {} ) holds
G ** F is MSUnTrans of g * f,A,C