ex f being ManySortedSet of A ex g being ManySortedSet of B st X = [f,g] by Def4;
hence X `1 is A -defined by MCART_1:7; :: thesis: verum