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