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 Element of 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 Element of 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 Element of 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 Element of NAT st
( 1 <= k & k < i & not q . k = p . k ) )
given j being Element of NAT such that A4: j in Seg n and
A5: q . j < p . j and
A6: for k being Element of NAT st 1 <= k & k < j holds
q . k = p . k ; :: thesis: contradiction
A7: ( 1 <= i & 1 <= j ) by A1, A4, FINSEQ_1:3;

per cases ( i < j or j < i or i = j ) by XXREAL_0:1;

suppose i < j ; :: thesis: contradiction

hence contradiction by A2, A6, A7; :: thesis: verum

end;

suppose j < i ; :: thesis: contradiction

hence contradiction by A3, A5, A7; :: thesis: verum

end;

suppose i = j ; :: thesis: contradiction

hence contradiction by A2, A5; :: thesis: verum

end;

end;