let n be Element of NAT ; :: thesis: for p, q being Element of n -tuples_on NAT holds
( p <= q or p > q )
let p, q be Element of n -tuples_on NAT ; :: thesis: ( p <= q or p > q )
assume A1: not p <= q ; :: thesis: p > q
then A2: ( not p < q & p <> q ) by Def2;
consider i being Element of NAT such that
A3: i in Seg n and
A4: p . i <> q . i and
A5: for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k by A1, Th6;
take i ; :: according to POLYNOM3:def 1 :: thesis: ( i in Seg n & q . i < p . i & ( for k being Element of NAT st 1 <= k & k < i holds
q . k = p . k ) )
thus i in Seg n by A3; :: thesis: ( q . i < p . i & ( for k being Element of NAT st 1 <= k & k < i holds
q . k = p . k ) )
p . i >= q . i by A2, A3, A5, Def1;
hence q . i < p . i by A4, XXREAL_0:1; :: thesis: for k being Element of NAT st 1 <= k & k < i holds
q . k = p . k
thus for k being Element of NAT st 1 <= k & k < i holds
q . k = p . k by A5; :: thesis: verum