consider f being ManySortedSet of A, g being ManySortedSet of B;
take [f,g] ; :: thesis: ex f being ManySortedSet of A ex g being ManySortedSet of B st [f,g] = [f,g]
take f ; :: thesis: ex g being ManySortedSet of B st [f,g] = [f,g]
take g ; :: thesis: [f,g] = [f,g]
thus [f,g] = [f,g] ; :: thesis: verum