let p, q be Element of n -tuples_on NAT; ( 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
; 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
; contradiction
A8:
1 <= j
by A5, FINSEQ_1:1;