consider f being ManySortedSet of , g being ManySortedSet of such that
A2: X = [f,g] by Def4;
thus ( X `2 is Function-like & X `2 is Relation-like ) by A2, MCART_1:7; :: thesis: verum