let a, b be set ; :: thesis: (a followed_by b) . 0 = a
dom (NAT --> b) = NAT ;
hence (a followed_by b) . 0 = a by Th30; :: thesis: verum