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