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 consider i being Element of NAT such that

A2: i in Seg n and

A3: p . i <> q . i and

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

p . k = q . k by Th6;

take i ; :: according to POLYNOM3:def 1 :: thesis: ( i in Seg n & q . i < p . i & ( for k being Nat st 1 <= k & k < i holds

q . k = p . k ) )

thus i in Seg n by A2; :: thesis: ( q . i < p . i & ( for k being Nat st 1 <= k & k < i holds

q . k = p . k ) )

not p < q by A1;

then p . i >= q . i by A2, A4;

hence q . i < p . i by A3, XXREAL_0:1; :: thesis: for k being Nat st 1 <= k & k < i holds

q . k = p . k

thus for k being Nat st 1 <= k & k < i holds

q . k = p . k by A4; :: thesis: verum

( 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 consider i being Element of NAT such that

A2: i in Seg n and

A3: p . i <> q . i and

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

p . k = q . k by Th6;

take i ; :: according to POLYNOM3:def 1 :: thesis: ( i in Seg n & q . i < p . i & ( for k being Nat st 1 <= k & k < i holds

q . k = p . k ) )

thus i in Seg n by A2; :: thesis: ( q . i < p . i & ( for k being Nat st 1 <= k & k < i holds

q . k = p . k ) )

not p < q by A1;

then p . i >= q . i by A2, A4;

hence q . i < p . i by A3, XXREAL_0:1; :: thesis: for k being Nat st 1 <= k & k < i holds

q . k = p . k

thus for k being Nat st 1 <= k & k < i holds

q . k = p . k by A4; :: thesis: verum