let a, b be Real_Sequence; ( ( for i being Nat holds
( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i ) ) implies IntervalSequence (a,b) is V238() )
assume A1:
for i being Nat holds
( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i )
; IntervalSequence (a,b) is V238()
now for n, m being Nat st n <= m holds
(IntervalSequence (a,b)) . m c= (IntervalSequence (a,b)) . nlet n,
m be
Nat;
( n <= m implies (IntervalSequence (a,b)) . m c= (IntervalSequence (a,b)) . n )assume A2:
n <= m
;
(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 ;
TARSKI:def 3 ( not x in product <*[.(a . m),(b . m).]*> or x in product <*[.(a . n),(b . n).]*> )
assume
x in product <*[.(a . m),(b . m).]*>
;
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 ( 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;
( 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;
for i being object st i in dom <*[.(a . n),(b . n).]*> holds
f . i in <*[.(a . n),(b . n).]*> . ihereby verum
let i be
object ;
( 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).]*>
;
f . i in <*[.(a . n),(b . n).]*> . ithen 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).]
by FINSEQ_1:def 8;
A11:
<*[.(a . n),(b . n).]*> . i = [.(a . n),(b . n).]
by A9, FINSEQ_1:def 8;
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;
verum
end; end;
hence
x in product <*[.(a . n),(b . n).]*>
by CARD_3:def 5;
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;
verum end;
hence
IntervalSequence (a,b) is V238()
by PROB_1:def 4; verum