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