defpred S_{1}[ Nat] means for p, q being Element of $1 -tuples_on NAT st p <> q holds

ex i being Element of NAT st

( i in Seg $1 & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) );

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
;

thus for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A22, A1); :: thesis: verum

ex i being Element of NAT st

( i in Seg $1 & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) );

A1: for n being Nat st S

S

proof

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

assume A2: for p, q being Element of n -tuples_on NAT st p <> q holds

ex i being Element of NAT st

( i in Seg n & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) ) ; :: thesis: S_{1}[n + 1]

let p, q be Element of (n + 1) -tuples_on NAT; :: thesis: ( p <> q implies ex i being Element of NAT st

( i in Seg (n + 1) & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) ) )

consider t1 being Element of n -tuples_on NAT, d1 being Element of NAT such that

A3: p = t1 ^ <*d1*> by FINSEQ_2:117;

assume A4: p <> q ; :: thesis: ex i being Element of NAT st

( i in Seg (n + 1) & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) )

consider t2 being Element of n -tuples_on NAT, d2 being Element of NAT such that

A5: q = t2 ^ <*d2*> by FINSEQ_2:117;

A6: len t1 = n by CARD_1:def 7;

A7: len t2 = n by CARD_1:def 7;

end;assume A2: for p, q being Element of n -tuples_on NAT st p <> q holds

ex i being Element of NAT st

( i in Seg n & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) ) ; :: thesis: S

let p, q be Element of (n + 1) -tuples_on NAT; :: thesis: ( p <> q implies ex i being Element of NAT st

( i in Seg (n + 1) & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) ) )

consider t1 being Element of n -tuples_on NAT, d1 being Element of NAT such that

A3: p = t1 ^ <*d1*> by FINSEQ_2:117;

assume A4: p <> q ; :: thesis: ex i being Element of NAT st

( i in Seg (n + 1) & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) )

consider t2 being Element of n -tuples_on NAT, d2 being Element of NAT such that

A5: q = t2 ^ <*d2*> by FINSEQ_2:117;

A6: len t1 = n by CARD_1:def 7;

A7: len t2 = n by CARD_1:def 7;

per cases
( t1 <> t2 or t1 = t2 )
;

end;

suppose
t1 <> t2
; :: thesis: ex i being Element of NAT st

( i in Seg (n + 1) & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) )

( i in Seg (n + 1) & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) )

then consider i being Element of NAT such that

A8: i in Seg n and

A9: t1 . i <> t2 . i and

A10: for k being Nat st 1 <= k & k < i holds

t1 . k = t2 . k by A2;

take i ; :: thesis: ( i in Seg (n + 1) & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) )

thus i in Seg (n + 1) by A8, FINSEQ_2:8; :: thesis: ( p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) )

i in dom t1 by A6, A8, FINSEQ_1:def 3;

then A11: p . i = t1 . i by A3, FINSEQ_1:def 7;

i in dom t2 by A7, A8, FINSEQ_1:def 3;

hence p . i <> q . i by A5, A9, A11, FINSEQ_1:def 7; :: thesis: for k being Nat st 1 <= k & k < i holds

p . k = q . k

let k be Nat; :: thesis: ( 1 <= k & k < i implies p . k = q . k )

assume that

A12: 1 <= k and

A13: k < i ; :: thesis: p . k = q . k

i <= n by A8, FINSEQ_1:1;

then A14: k <= n by A13, XXREAL_0:2;

then A15: k in dom t1 by A6, A12, FINSEQ_3:25;

A16: k in dom t2 by A7, A12, A14, FINSEQ_3:25;

t1 . k = t2 . k by A10, A12, A13;

hence p . k = t2 . k by A3, A15, FINSEQ_1:def 7

.= q . k by A5, A16, FINSEQ_1:def 7 ;

:: thesis: verum

end;A8: i in Seg n and

A9: t1 . i <> t2 . i and

A10: for k being Nat st 1 <= k & k < i holds

t1 . k = t2 . k by A2;

take i ; :: thesis: ( i in Seg (n + 1) & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) )

thus i in Seg (n + 1) by A8, FINSEQ_2:8; :: thesis: ( p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) )

i in dom t1 by A6, A8, FINSEQ_1:def 3;

then A11: p . i = t1 . i by A3, FINSEQ_1:def 7;

i in dom t2 by A7, A8, FINSEQ_1:def 3;

hence p . i <> q . i by A5, A9, A11, FINSEQ_1:def 7; :: thesis: for k being Nat st 1 <= k & k < i holds

p . k = q . k

let k be Nat; :: thesis: ( 1 <= k & k < i implies p . k = q . k )

assume that

A12: 1 <= k and

A13: k < i ; :: thesis: p . k = q . k

i <= n by A8, FINSEQ_1:1;

then A14: k <= n by A13, XXREAL_0:2;

then A15: k in dom t1 by A6, A12, FINSEQ_3:25;

A16: k in dom t2 by A7, A12, A14, FINSEQ_3:25;

t1 . k = t2 . k by A10, A12, A13;

hence p . k = t2 . k by A3, A15, FINSEQ_1:def 7

.= q . k by A5, A16, FINSEQ_1:def 7 ;

:: thesis: verum

suppose A17:
t1 = t2
; :: thesis: ex i being Element of NAT st

( i in Seg (n + 1) & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) )

( i in Seg (n + 1) & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) )

take i = n + 1; :: thesis: ( i in Seg (n + 1) & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) )

thus i in Seg (n + 1) by FINSEQ_1:4; :: thesis: ( p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) )

p . i = d1 by A3, FINSEQ_2:116;

hence p . i <> q . i by A3, A5, A4, A17, FINSEQ_2:116; :: thesis: for k being Nat st 1 <= k & k < i holds

p . k = q . k

let k be Nat; :: thesis: ( 1 <= k & k < i implies p . k = q . k )

assume that

A18: 1 <= k and

A19: k < i ; :: thesis: p . k = q . k

A20: k <= n by A19, NAT_1:13;

then A21: k in dom t2 by A7, A18, FINSEQ_3:25;

k in dom t1 by A6, A18, A20, FINSEQ_3:25;

hence p . k = t2 . k by A3, A17, FINSEQ_1:def 7

.= q . k by A5, A21, FINSEQ_1:def 7 ;

:: thesis: verum

end;p . k = q . k ) )

thus i in Seg (n + 1) by FINSEQ_1:4; :: thesis: ( p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds

p . k = q . k ) )

p . i = d1 by A3, FINSEQ_2:116;

hence p . i <> q . i by A3, A5, A4, A17, FINSEQ_2:116; :: thesis: for k being Nat st 1 <= k & k < i holds

p . k = q . k

let k be Nat; :: thesis: ( 1 <= k & k < i implies p . k = q . k )

assume that

A18: 1 <= k and

A19: k < i ; :: thesis: p . k = q . k

A20: k <= n by A19, NAT_1:13;

then A21: k in dom t2 by A7, A18, FINSEQ_3:25;

k in dom t1 by A6, A18, A20, FINSEQ_3:25;

hence p . k = t2 . k by A3, A17, FINSEQ_1:def 7

.= q . k by A5, A21, FINSEQ_1:def 7 ;

:: thesis: verum

thus for n being Nat holds S