ex f being ManySortedSet of ex g being ManySortedSet of st X = [f,g] by Def4;
hence ( X `1 is Function-like & X `1 is Relation-like ) by MCART_1:7; :: thesis: verum