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;

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

suppose i < j ; :: thesis: contradiction

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

end;

suppose j < i ; :: thesis: contradiction

hence contradiction by A3, A6, A8; :: thesis: verum

end;

suppose i = j ; :: thesis: contradiction

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

end;

end;