consider f being ManySortedSet of , g being ManySortedSet of such that
A2: X = [f,g] by Def4;
thus X `2 is B -defined by A2, MCART_1:7; :: thesis: verum