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 S₁[ 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 S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[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 S₂[ Nat] means ( $1 in dom p implies p . $1 = p . 1 );
A9: for w being Nat st S₂[w] holds
S₂[w + 1]

proof

let w be Nat; :: thesis: ( S₂[w] implies S₂[w + 1] )
assume A10: S₂[w] ; :: thesis: S₂[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: S₂[ 0 ] by FINSEQ_3:24;
A13: for k being Nat holds S₂[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: S₁[ 0 ] by FINSEQ_3:24;
for k being Nat holds S₁[k] from NAT_1:sch 2(A14, A3);
hence p . i = p . j by A1; :: thesis: verum