let p be FinSequence; :: thesis: for i, j being Nat st i in dom p & j in dom p & ( for k being Nat st k in dom p & k + 1 in dom p holds
p . k = p . (k + 1) ) holds
p . i = p . j
let i, j be Nat; :: thesis: ( i in dom p & j in dom p & ( for k being Nat st k in dom p & k + 1 in dom p holds
p . k = p . (k + 1) ) implies p . i = p . j )
assume that
A1: ( i in dom p & j in dom p ) and
A2: for k being Nat st k in dom p & k + 1 in dom p holds
p . k = p . (k + 1) ; :: thesis: p . i = p . j
defpred S1[ Nat] means for j being Nat st $1 in dom p & j in dom p holds
p . $1 = p . j;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
let j be Nat; :: thesis: ( k + 1 in dom p & j in dom p implies p . (k + 1) = p . j )
assume that
A5: k + 1 in dom p and
A6: j in dom p ; :: thesis: p . (k + 1) = p . j
per cases ( k in dom p or not k in dom p ) ;
suppose A7: k in dom p ; :: thesis: p . (k + 1) = p . j
hence p . (k + 1) = p . k by A2, A5
.= p . j by A4, A6, A7 ;
:: thesis: verum
end;
suppose A8: not k in dom p ; :: thesis: p . (k + 1) = p . j
defpred S2[ Nat] means ( $1 in dom p implies p . $1 = p . 1 );
A9: for w being Nat st S2[w] holds
S2[w + 1]
proof
let w be Nat; :: thesis: ( S2[w] implies S2[w + 1] )
assume A10: S2[w] ; :: thesis: S2[w + 1]
assume A11: w + 1 in dom p ; :: thesis: p . (w + 1) = p . 1
per cases ( w in dom p or not w in dom p ) ;
suppose w in dom p ; :: thesis: p . (w + 1) = p . 1
hence p . (w + 1) = p . 1 by A2, A10, A11; :: thesis: verum
end;
suppose not w in dom p ; :: thesis: p . (w + 1) = p . 1
then w = 0 by A11, Th1;
hence p . (w + 1) = p . 1 ; :: thesis: verum
end;
end;
end;
A12: S2[ 0 ] by FINSEQ_3:24;
A13: for k being Nat holds S2[k] from NAT_1:sch 2(A12, A9);
 k = 0 by A5, A8, Th1;
hence p . (k + 1) = p . j by A6, A13; :: thesis: verum
end;
end;
end;
A14: S1[ 0 ] by FINSEQ_3:24;
for k being Nat holds S1[k] from NAT_1:sch 2(A14, A3);
 hence p . i = p . j by A1; :: thesis: verum