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_{1}[ 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_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by FINSEQ_3:24;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A14, A3);

hence p . i = p . j by A1; :: thesis: verum

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

p . $1 = p . j;

A3: for k being Nat st S

S

proof

A14:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[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

end;assume A4: S

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 )
;

end;

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

defpred S_{2}[ Nat] means ( $1 in dom p implies p . $1 = p . 1 );

A9: for w being Nat st S_{2}[w] holds

S_{2}[w + 1]
_{2}[ 0 ]
by FINSEQ_3:24;

A13: for k being Nat holds S_{2}[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;A9: for w being Nat st S

S

proof

A12:
S
let w be Nat; :: thesis: ( S_{2}[w] implies S_{2}[w + 1] )

assume A10: S_{2}[w]
; :: thesis: S_{2}[w + 1]

assume A11: w + 1 in dom p ; :: thesis: p . (w + 1) = p . 1

end;assume A10: S

assume A11: w + 1 in dom p ; :: thesis: p . (w + 1) = p . 1

A13: for k being Nat holds S

k = 0 by A5, A8, Th1;

hence p . (k + 1) = p . j by A6, A13; :: thesis: verum

for k being Nat holds S

hence p . i = p . j by A1; :: thesis: verum