let a, b be set ; :: thesis: dom ((NAT --> a) +* (NAT .--> b)) = NAT \/ {NAT }
thus dom ((NAT --> a) +* (NAT .--> b)) = (dom (NAT --> a)) \/ (dom (NAT .--> b)) by FUNCT_4:def 1
.= NAT \/ (dom (NAT .--> b)) by FUNCOP_1:19
.= NAT \/ {NAT } by FUNCOP_1:19 ; :: thesis: verum