set g = the ManySortedCategory of A;
set f = the ManySortedFunctor of the ManySortedCategory of A * F, the ManySortedCategory of A * G;
take I = [ the ManySortedCategory of A, the ManySortedFunctor of the ManySortedCategory of A * F, the ManySortedCategory of A * G]; :: thesis: I `2 is ManySortedFunctor of (I `1) * F,(I `1) * G
I `1 = the ManySortedCategory of A by MCART_1:7;
hence I `2 is ManySortedFunctor of (I `1) * F,(I `1) * G by MCART_1:7; :: thesis: verum