let a, b be Real_Sequence; :: thesis: 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); :: thesis: ( 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 ) ) ; :: thesis: for i being Nat holds
( a . i = a . 0 & b . i = b . 0 & (diameter S) . i = 0 )
defpred S₁[ Nat] means ( a . $1 = a . 0 & b . $1 = b . 0 );
A4: S₁[ 0 ] ;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[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 S₁[k + 1] by A1, A6; :: thesis: verum

end;

A7: for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A5);
let i be Nat; :: thesis: ( a . i = a . 0 & b . i = b . 0 & (diameter S) . i = 0 )
thus A8: a . i = a . 0 by A7; :: thesis: ( b . i = b . 0 & (diameter S) . i = 0 )
thus A9: b . i = b . 0 by A7; :: thesis: (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; :: thesis: verum