set B = M | A;
A1: dom (M | A) = (dom M) /\ A by RELAT_1:90;
dom M = I by PBOOLE:def 3;
then dom (M | A) = A by A1, XBOOLE_1:28;
hence M | A is ManySortedSet of A by PBOOLE:def 3; :: thesis: verum