consider g being ManySortedFunction of B;
consider f being ManySortedCategory of A;
reconsider X = [f,g] as ManySortedSet of A,B ;
take X ; :: thesis: ( X is Category-yielding_on_first & X is Function-yielding_on_second )
thus ( X `1 is Category-yielding & X `2 is Function-yielding ) by MCART_1:7; :: according to INDEX_1:def 5,INDEX_1:def 6 :: thesis: verum