defpred S₁[ 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 Element of NAT st 1 <= k & k < i holds
p . k = q . k ) );
A1: S₁[ 0 ]

proof

let p, q be Element of 0 -tuples_on NAT ; :: thesis: ( p <> q implies ex i being Element of NAT st
( i in Seg 0 & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) ) )
assume that
A2: p <> q and
for i being Element of NAT holds
( not i in Seg 0 or not p . i <> q . i or ex k being Element of NAT st
( 1 <= k & k < i & not p . k = q . k ) ) ; :: thesis: contradiction
( p = <*> NAT & q = <*> NAT ) by FINSEQ_2:113;
hence contradiction by A2; :: thesis: verum

end;

A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: 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 Element of NAT st 1 <= k & k < i holds
p . k = q . k ) ) ; :: thesis: S₁[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 Element of 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
A5: p = t1 ^ <*d1*> by FINSEQ_2:137;
consider t2 being Element of n -tuples_on NAT , d2 being Element of NAT such that
A6: q = t2 ^ <*d2*> by FINSEQ_2:137;
assume A7: p <> q ; :: thesis: ex i being Element of NAT st
( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) )
A8: ( len t1 = n & len t2 = n ) by FINSEQ_1:def 18;

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 Element of NAT st 1 <= k & k < i holds
p . k = q . k ) )

then consider i being Element of NAT such that
A9: i in Seg n and
A10: t1 . i <> t2 . i and
A11: for k being Element of NAT st 1 <= k & k < i holds
t1 . k = t2 . k by A4;
take i ; :: thesis: ( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) )
thus i in Seg (n + 1) by A9, FINSEQ_2:9; :: thesis: ( p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) )
( i in dom t1 & i in dom t2 ) by A8, A9, FINSEQ_1:def 3;
then ( p . i = t1 . i & q . i = t2 . i ) by A5, A6, FINSEQ_1:def 7;
hence p . i <> q . i by A10; :: thesis: for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k
let k be Element of 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
A14: t1 . k = t2 . k by A11, A12, A13;
i <= n by A9, FINSEQ_1:3;
then k <= n by A13, XXREAL_0:2;
then A15: ( k in dom t1 & k in dom t2 ) by A8, A12, FINSEQ_3:27;
hence p . k = t2 . k by A5, A14, FINSEQ_1:def 7
.= q . k by A6, A15, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose A16: t1 = t2 ; :: thesis: ex i being Element of NAT st
( i in Seg (n + 1) & p . i <> q . i & ( for k being Element of 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 Element of NAT st 1 <= k & k < i holds
p . k = q . k ) )
thus i in Seg (n + 1) by FINSEQ_1:6; :: thesis: ( p . i <> q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) )
( p . i = d1 & q . i = d2 ) by A5, A6, FINSEQ_2:136;
hence p . i <> q . i by A5, A6, A7, A16; :: thesis: for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k
let k be Element of NAT ; :: thesis: ( 1 <= k & k < i implies p . k = q . k )
assume that
A17: 1 <= k and
A18: k < i ; :: thesis: p . k = q . k
k <= n by A18, NAT_1:13;
then A19: ( k in dom t1 & k in dom t2 ) by A8, A17, FINSEQ_3:27;
hence p . k = t2 . k by A5, A16, FINSEQ_1:def 7
.= q . k by A6, A19, FINSEQ_1:def 7 ;
:: thesis: verum

end;

end;

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A3); :: thesis: verum