let a, b, c be set ; :: thesis: ((a,b) followed_by c) . 1 = b
dom ((0,1) --> (a,b)) = {0,1} by FUNCT_4:62;
then A1: 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 A1, FUNCT_4:13
.= b by FUNCT_4:63 ; :: thesis: verum