let a, b, c be set ; :: thesis: dom (a,b followed_by c) = NAT
thus dom (a,b followed_by c) = (dom (NAT --> c)) \/ (dom (0 ,1 --> a,b)) by FUNCT_4:def 1
.= NAT \/ (dom (0 ,1 --> a,b)) by FUNCOP_1:19
.= NAT \/ {0 ,1} by FUNCT_4:65
.= NAT by XBOOLE_1:12 ; :: thesis: verum