set g = the ManySortedFunction of B;
set f = the ManySortedCategory of A;
reconsider X = [ the ManySortedCategory of A, the ManySortedFunction of B] 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 ) ; :: according to INDEX_1:def 5,INDEX_1:def 6 :: thesis: verum