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
thus I `2 is ManySortedFunctor of (I `1) * F,(I `1) * G ; :: thesis: verum