let p, q be Element of n -tuples_on NAT; :: thesis: ( 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 ) ) implies for i being Element of NAT holds

( not i in Seg n or not q . i < p . i or ex k being Nat st

( 1 <= k & k < i & not q . k = p . k ) ) )

given i being Element of NAT such that A1: i in Seg n and

A2: p . i < q . i and

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

p . k = q . k ; :: thesis: for i being Element of NAT holds

( not i in Seg n or not q . i < p . i or ex k being Nat st

( 1 <= k & k < i & not q . k = p . k ) )

A4: 1 <= i by A1, FINSEQ_1:1;

given j being Element of NAT such that A5: j in Seg n and

A6: q . j < p . j and

A7: for k being Nat st 1 <= k & k < j holds

q . k = p . k ; :: thesis: contradiction

A8: 1 <= j by A5, FINSEQ_1:1;

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

p . k = q . k ) ) implies for i being Element of NAT holds

( not i in Seg n or not q . i < p . i or ex k being Nat st

( 1 <= k & k < i & not q . k = p . k ) ) )

given i being Element of NAT such that A1: i in Seg n and

A2: p . i < q . i and

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

p . k = q . k ; :: thesis: for i being Element of NAT holds

( not i in Seg n or not q . i < p . i or ex k being Nat st

( 1 <= k & k < i & not q . k = p . k ) )

A4: 1 <= i by A1, FINSEQ_1:1;

given j being Element of NAT such that A5: j in Seg n and

A6: q . j < p . j and

A7: for k being Nat st 1 <= k & k < j holds

q . k = p . k ; :: thesis: contradiction

A8: 1 <= j by A5, FINSEQ_1:1;