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