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; :: thesis: ( 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 ) ) ; :: thesis: S1[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;
per cases ( t1 <> t2 or t1 = t2 ) ;
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 ) )

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 ; :: thesis: ( p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) )

i in dom t1 by ;
then A11: p . i = t1 . i by ;
i in dom t2 by ;
hence p . i <> q . i by ; :: 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 ;
then A14: k <= n by ;
then A15: k in dom t1 by ;
A16: k in dom t2 by ;
t1 . k = t2 . k by ;
hence p . k = t2 . k by
.= q . k by ;
:: thesis: verum
end;
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 ) )

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 ;
hence p . i <> q . i by ; :: 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 ;
then A21: k in dom t2 by ;
k in dom t1 by ;
hence p . k = t2 . k by
.= q . k by ;
:: thesis: verum
end;
end;
end;
A22: S1[ 0 ] ;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A22, A1); :: thesis: verum