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