let a, b, c be set ; :: thesis: for n being Nat st n > 1 holds
((a,b) followed_by c) . n = c
let n be Nat; :: thesis: ( n > 1 implies ((a,b) followed_by c) . n = c )
assume A1: n > 1 ; :: thesis: ((a,b) followed_by c) . n = c
dom ((0,1) --> (a,b)) = {0,1} by FUNCT_4:62;
then A2: not n in dom ((0,1) --> (a,b)) by A1, TARSKI:def 2;
A3: n in NAT by ORDINAL1:def 12;
thus ((a,b) followed_by c) . n = ((NAT --> c) +* ((0,1) --> (a,b))) . n
.= (NAT --> c) . n by A2, FUNCT_4:11
.= c by A3, FUNCOP_1:7 ; :: thesis: verum