defpred S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[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 ) )
;
S1[n + 1]
let p,
q be
Element of
(n + 1) -tuples_on NAT;
( 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
;
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 )
;
suppose
t1 <> t2
;
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 ) )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
;
( 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;
( 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;
for k being Nat st 1 <= k & k < i holds
p . k = q . klet k be
Nat;
( 1 <= k & k < i implies p . k = q . k )assume that A12:
1
<= k
and A13:
k < i
;
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
;
verum end; suppose A17:
t1 = t2
;
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 ) )take i =
n + 1;
( 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;
( 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;
for k being Nat st 1 <= k & k < i holds
p . k = q . klet k be
Nat;
( 1 <= k & k < i implies p . k = q . k )assume that A18:
1
<= k
and A19:
k < i
;
p . k = q . kA20:
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
;
verum end;
end;
A22:
S1[ 0 ]
;
thus
for n being Nat holds S1[n]
from NAT_1:sch 2(A22, A1); verum