let I1 be set ; :: thesis: 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
let I2, I3 be non empty set ; :: thesis: 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
let f be Function of I1,I2; :: thesis: 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
let g be Function of I2,I3; :: thesis: 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
let B be ManySortedSet of I2; :: thesis: 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
let C be ManySortedSet of I3; :: thesis: for G being MSUnTrans of g,B,C holds G * f is MSUnTrans of g * f,B * f,C
let G be MSUnTrans of g,B,C; :: thesis: G * f is MSUnTrans of g * f,B * f,C
A1: C * (g * f) = (C * g) * f by RELAT_1:36;
G is ManySortedFunction of B,C * g by Def4;
hence G * f is ManySortedFunction of B * f,C * (g * f) by A1, ALTCAT_2:5; :: according to FUNCTOR0:def 4 :: thesis: verum