let a, b, c be set ; :: thesis: (a,b followed_by c) . 0 = a
dom (0 ,1 --> a,b) = {0 ,1} by FUNCT_4:65;
then A1: 0 in dom (0 ,1 --> a,b) by TARSKI:def 2;
thus (a,b followed_by c) . 0 = ((NAT --> c) +* (0 ,1 --> a,b)) . 0
.= (0 ,1 --> a,b) . 0 by A1, FUNCT_4:14
.= a by FUNCT_4:66 ; :: thesis: verum