let a, b, c be set ; for n being Nat st n > 1 holds
((a,b) followed_by c) . n = c
let n be Nat; ( n > 1 implies ((a,b) followed_by c) . n = c )
assume A1:
n > 1
; ((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
; verum