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:65;
then A2: not n in dom (0 ,1 --> a,b) by A1, TARSKI:def 2;
A3: n in NAT by ORDINAL1:def 13;
thus (a,b followed_by c) . n = ((NAT --> c) +* (0 ,1 --> a,b)) . n
.= (NAT --> c) . n by A2, FUNCT_4:12
.= c by A3, FUNCOP_1:13 ; :: thesis: verum