let a, b be Real_Sequence; for S being SetSequence of (Euclid 1) st a . 0 = b . 0 & S = IntervalSequence (a,b) & ( for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ) holds
for i being Nat holds
( a . i = a . 0 & b . i = b . 0 & (diameter S) . i = 0 )
let S be SetSequence of (Euclid 1); ( a . 0 = b . 0 & S = IntervalSequence (a,b) & ( for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ) implies for i being Nat holds
( a . i = a . 0 & b . i = b . 0 & (diameter S) . i = 0 ) )
assume that
A1:
a . 0 = b . 0
and
A2:
S = IntervalSequence (a,b)
and
A3:
for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) )
; for i being Nat holds
( a . i = a . 0 & b . i = b . 0 & (diameter S) . i = 0 )
defpred S1[ Nat] means ( a . $1 = a . 0 & b . $1 = b . 0 );
A4:
S1[ 0 ]
;
A5:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A6:
S1[
k]
;
S1[k + 1]
( (
a . (k + 1) = a . k &
b . (k + 1) = ((a . k) + (b . k)) / 2 ) or (
a . (k + 1) = ((a . k) + (b . k)) / 2 &
b . (k + 1) = b . k ) )
by A3;
hence
S1[
k + 1]
by A1, A6;
verum
end;
A7:
for k being Nat holds S1[k]
from NAT_1:sch 2(A4, A5);
let i be Nat; ( a . i = a . 0 & b . i = b . 0 & (diameter S) . i = 0 )
thus A8:
a . i = a . 0
by A7; ( b . i = b . 0 & (diameter S) . i = 0 )
thus A9:
b . i = b . 0
by A7; (diameter S) . i = 0
(diameter S) . i = (b . i) - (a . i)
by A1, A2, A3, Th28;
hence
(diameter S) . i = 0
by A1, A8, A9; verum