let n be Element of NAT ; :: thesis: for p, q, r being Element of n -tuples_on NAT holds

( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )

let p, q, r be Element of n -tuples_on NAT; :: thesis: ( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )

thus A1: ( p < q & q < r implies p < r ) :: thesis: ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r )

( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )

let p, q, r be Element of n -tuples_on NAT; :: thesis: ( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )

thus A1: ( p < q & q < r implies p < r ) :: thesis: ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r )

proof

assume A17:
( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) )
; :: thesis: p <= r
assume that

A2: p < q and

A3: q < r ; :: thesis: p < r

consider i being Element of NAT such that

A4: i in Seg n and

A5: p . i < q . i and

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

p . k = q . k by A2;

consider j being Element of NAT such that

A7: j in Seg n and

A8: q . j < r . j and

A9: for k being Nat st 1 <= k & k < j holds

q . k = r . k by A3;

reconsider t = min (i,j) as Element of NAT ;

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

p . k = r . k ) )

thus t in Seg n by A4, A7, XXREAL_0:15; :: thesis: ( p . t < r . t & ( for k being Nat st 1 <= k & k < t holds

p . k = r . k ) )

p . k = r . k

let k be Nat; :: thesis: ( 1 <= k & k < t implies p . k = r . k )

assume that

A14: 1 <= k and

A15: k < t ; :: thesis: p . k = r . k

t <= j by XXREAL_0:17;

then A16: k < j by A15, XXREAL_0:2;

t <= i by XXREAL_0:17;

then k < i by A15, XXREAL_0:2;

hence p . k = q . k by A6, A14

.= r . k by A9, A14, A16 ;

:: thesis: verum

end;A2: p < q and

A3: q < r ; :: thesis: p < r

consider i being Element of NAT such that

A4: i in Seg n and

A5: p . i < q . i and

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

p . k = q . k by A2;

consider j being Element of NAT such that

A7: j in Seg n and

A8: q . j < r . j and

A9: for k being Nat st 1 <= k & k < j holds

q . k = r . k by A3;

reconsider t = min (i,j) as Element of NAT ;

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

p . k = r . k ) )

thus t in Seg n by A4, A7, XXREAL_0:15; :: thesis: ( p . t < r . t & ( for k being Nat st 1 <= k & k < t holds

p . k = r . k ) )

now :: thesis: p . t < r . tend;

hence
p . t < r . t
; :: thesis: for k being Nat st 1 <= k & k < t holds per cases
( i < j or i > j or i = j )
by XXREAL_0:1;

end;

suppose A10:
i < j
; :: thesis: p . t < r . t

A11:
i >= 1
by A4, FINSEQ_1:1;

t = i by A10, XXREAL_0:def 9;

hence p . t < r . t by A5, A9, A10, A11; :: thesis: verum

end;t = i by A10, XXREAL_0:def 9;

hence p . t < r . t by A5, A9, A10, A11; :: thesis: verum

suppose A12:
i > j
; :: thesis: p . t < r . t

A13:
j >= 1
by A7, FINSEQ_1:1;

t = j by A12, XXREAL_0:def 9;

hence p . t < r . t by A6, A8, A12, A13; :: thesis: verum

end;t = j by A12, XXREAL_0:def 9;

hence p . t < r . t by A6, A8, A12, A13; :: thesis: verum

p . k = r . k

let k be Nat; :: thesis: ( 1 <= k & k < t implies p . k = r . k )

assume that

A14: 1 <= k and

A15: k < t ; :: thesis: p . k = r . k

t <= j by XXREAL_0:17;

then A16: k < j by A15, XXREAL_0:2;

t <= i by XXREAL_0:17;

then k < i by A15, XXREAL_0:2;

hence p . k = q . k by A6, A14

.= r . k by A9, A14, A16 ;

:: thesis: verum