let a, b be Real_Sequence; :: thesis: ( ( for i being Nat holds
( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i ) ) implies IntervalSequence (a,b) is non-ascending )
assume A1: for i being Nat holds
( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i ) ; :: thesis: IntervalSequence (a,b) is non-ascending

now :: thesis: for n, m being Nat st n <= m holds
(IntervalSequence (a,b)) . m c= (IntervalSequence (a,b)) . n

let n, m be Nat; :: thesis: ( n <= m implies (IntervalSequence (a,b)) . m c= (IntervalSequence (a,b)) . n )
assume A2: n <= m ; :: thesis: (IntervalSequence (a,b)) . m c= (IntervalSequence (a,b)) . n
product <*[.(a . m),(b . m).]*> c= product <*[.(a . n),(b . n).]*>

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product <*[.(a . m),(b . m).]*> or x in product <*[.(a . n),(b . n).]*> )
assume x in product <*[.(a . m),(b . m).]*> ; :: thesis: x in product <*[.(a . n),(b . n).]*>
then consider f being Function such that
A3: x = f and
A4: dom f = dom <*[.(a . m),(b . m).]*> and
A5: for i being object st i in dom <*[.(a . m),(b . m).]*> holds
f . i in <*[.(a . m),(b . m).]*> . i by CARD_3:def 5;
A6: dom <*[.(a . m),(b . m).]*> = Seg 1 by FINSEQ_1:def 8;

now :: thesis: ( x = f & dom f = dom <*[.(a . n),(b . n).]*> & ( for i being object st i in dom <*[.(a . n),(b . n).]*> holds
f . i in <*[.(a . n),(b . n).]*> . i ) )

thus x = f by A3; :: thesis: ( dom f = dom <*[.(a . n),(b . n).]*> & ( for i being object st i in dom <*[.(a . n),(b . n).]*> holds
f . i in <*[.(a . n),(b . n).]*> . i ) )
thus dom f = dom <*[.(a . n),(b . n).]*> by A6, A4, FINSEQ_1:def 8; :: thesis: for i being object st i in dom <*[.(a . n),(b . n).]*> holds
f . i in <*[.(a . n),(b . n).]*> . i

hereby :: thesis: verum

let i be object ; :: thesis: ( i in dom <*[.(a . n),(b . n).]*> implies f . i in <*[.(a . n),(b . n).]*> . i )
assume A7: i in dom <*[.(a . n),(b . n).]*> ; :: thesis: f . i in <*[.(a . n),(b . n).]*> . i
then A8: i in dom <*[.(a . m),(b . m).]*> by A6, FINSEQ_1:def 8;
i in Seg 1 by A7, FINSEQ_1:def 8;
then A9: i = 1 by TARSKI:def 1, FINSEQ_1:2;
then A10: <*[.(a . m),(b . m).]*> . i = [.(a . m),(b . m).] ;
A11: <*[.(a . n),(b . n).]*> . i = [.(a . n),(b . n).] by A9;
A12: a is non-decreasing by A1;
dom a = NAT by SEQ_1:1;
then ( n in dom a & m in dom a ) by ORDINAL1:def 12;
then A13: a . n <= a . m by A12, A2;
A14: b is non-increasing by A1;
dom b = NAT by SEQ_1:1;
then ( n in dom b & m in dom b ) by ORDINAL1:def 12;
then b . m <= b . n by A14, A2;
then [.(a . m),(b . m).] c= [.(a . n),(b . n).] by A13, XXREAL_1:34;
hence f . i in <*[.(a . n),(b . n).]*> . i by A8, A5, A10, A11; :: thesis: verum

end;

end;

hence x in product <*[.(a . n),(b . n).]*> by CARD_3:def 5; :: thesis: verum

end;

then (IntervalSequence (a,b)) . m c= product <*[.(a . n),(b . n).]*> by Def1;
hence (IntervalSequence (a,b)) . m c= (IntervalSequence (a,b)) . n by Def1; :: thesis: verum

end;

hence IntervalSequence (a,b) is non-ascending by PROB_1:def 4; :: thesis: verum