let B, C, D, b, c, d be set ; :: thesis: dom (((B .--> b) +* (C .--> c)) +* (D .--> d)) = {B,C,D}
A1: dom ((B .--> b) +* (C .--> c)) = (dom (B .--> b)) \/ (dom (C .--> c)) by FUNCT_4:def 1;
A2: dom (B .--> b) = {B} by FUNCOP_1:19;
A3: dom (C .--> c) = {C} by FUNCOP_1:19;
dom (D .--> d) = {D} by FUNCOP_1:19;
hence dom (((B .--> b) +* (C .--> c)) +* (D .--> d)) = ({B} \/ {C}) \/ {D} by A1, A2, A3, FUNCT_4:def 1
.= {B,C} \/ {D} by ENUMSET1:41
.= {B,C,D} by ENUMSET1:43 ;
:: thesis: verum