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: S₁[ 0 ] by FINSEQ_3:26;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: 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
A6: k + 1 in dom p and
A7: j in dom p ; :: thesis: p . (k + 1) = p . j

per cases ( k in dom p or not k in dom p ) ;

suppose A8: k in dom p ; :: thesis: p . (k + 1) = p . j

hence p . (k + 1) = p . k by A2, A6
.= p . j by A5, A7, A8 ;
:: thesis: verum

end;

suppose not k in dom p ; :: thesis: p . (k + 1) = p . j

then A9: k = 0 by A6, Th1;
defpred S₂[ Nat] means ( $1 in dom p implies p . $1 = p . 1 );
A10: S₂[ 0 ] by FINSEQ_3:26;
A11: for w being Nat st S₂[w] holds
S₂[w + 1]

proof

let w be Nat; :: thesis: ( S₂[w] implies S₂[w + 1] )
assume A12: S₂[w] ; :: thesis: S₂[w + 1]
assume A13: 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, A12, A13; :: thesis: verum

end;

suppose not w in dom p ; :: thesis: p . (w + 1) = p . 1

then w = 0 by A13, Th1;
hence p . (w + 1) = p . 1 ; :: thesis: verum

end;

end;

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A10, A11);
hence p . (k + 1) = p . j by A7, A9; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
hence p . i = p . j by A1; :: thesis: verum