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