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