let a, b, c be set ; ((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
; verum