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