let A, B, x be set ; :: thesis: dom ((id A) +* (B --> x)) = A \/ B
dom ((id A) +* (B --> x)) = (dom (id A)) \/ (dom (B --> x)) by FUNCT_4:def 1;
then dom ((id A) +* (B --> x)) = A \/ (dom (B --> x)) ;
hence dom ((id A) +* (B --> x)) = A \/ B by FUNCOP_1:13; :: thesis: verum