A1: ( dom b1 = X & dom b2 = X ) by PBOOLE:def 3;
X /\ X = X ;
hence dom (b1 + b2) = X by A1, VALUED_1:def 1; :: according to PBOOLE:def 3 :: thesis: verum