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