let a, b be set ; :: thesis: dom (a followed_by b) = NAT
thus dom (a followed_by b) = dom ((NAT --> b) +* 0 ,a)
.= dom (NAT --> b) by Th32
.= NAT by FUNCOP_1:19 ; :: thesis: verum