let a, b be Real_Sequence; :: thesis: ( a . 0 <= b . 0 & ( 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 <= b . i )
assume that
A1: a . 0 <= b . 0 and
A2: 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 <= b . i
defpred S₁[ object ] means ex i being Nat st
( $1 = i & a . i <= b . i );
A3: S₁[ 0 ] by A1;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider i being Nat such that
k = i and
A5: a . k <= b . k ;
( ( 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 A2;
hence S₁[k + 1] by A5, Th8; :: thesis: verum

end;

A6: for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
let k be Nat; :: thesis: a . k <= b . k
ex i being Nat st
( i = k & a . i <= b . i ) by A6;
hence a . k <= b . k ; :: thesis: verum