A1: X /\ X = X ;
( dom b1 = X & dom b2 = X ) by PARTFUN1:def 2;
then dom (b1 + b2) = X by A1, VALUED_1:def 1;
hence b1 + b2 is ManySortedSet of X by PARTFUN1:def 2, RELAT_1:def 18; :: thesis: verum