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 B being ManySortedSet of I2
for C being ManySortedSet of I3
for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C