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