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)))
.= NAT \/ {0,1} by FUNCT_4:62
.= NAT by XBOOLE_1:12 ; :: thesis: verum