let a, b be Real; :: thesis: ( 0 < a & ( for e being Real st 0 < e holds
((a + e) ") * a <= b ) implies 1 <= b )
assume A1: ( 0 < a & ( for e being Real st 0 < e holds
((a + e) ") * a <= b ) ) ; :: thesis: 1 <= b
set B = seq_const b;
A2P: (seq_const b) . 1 = b ;
deffunc H₁( Nat) -> set = 1 / ($1 + 1);
consider E being Real_Sequence such that
A3: for n being Nat holds E . n = H₁(n) from SEQ_1:sch 1();
A4: ( E is convergent & lim E = 0 ) by A3, SEQ_4:31;
set A = seq_const a;
(seq_const a) . 1 = a ;
then A5: ( seq_const a is convergent & lim (seq_const a) = a ) by SEQ_4:25;
A6: ( (seq_const a) + E is convergent & lim ((seq_const a) + E) = a + 0 ) by A4, A5, SEQ_2:6;
for n being Nat holds ((seq_const a) + E) . n <> 0

proof

let n be Nat; :: thesis: ((seq_const a) + E) . n <> 0
A7: (seq_const a) . n = a by SEQ_1:57;
((seq_const a) + E) . n = ((seq_const a) . n) + (E . n) by SEQ_1:7
.= a + (1 / (n + 1)) by A7, A3 ;
hence ((seq_const a) + E) . n <> 0 by A1; :: thesis: verum

end;

then A9: ( ((seq_const a) + E) " is convergent & lim (((seq_const a) + E) ") = a " ) by A6, A1, SEQ_2:21, SEQ_2:22, SEQ_1:5;
A11: lim ((((seq_const a) + E) ") (#) (seq_const a)) = (a ") * a by A5, A9, SEQ_2:15
.= 1 by A1, XCMPLX_0:def 7 ;
for n being Nat holds ((((seq_const a) + E) ") (#) (seq_const a)) . n <= (seq_const b) . n

proof

let n be Nat; :: thesis: ((((seq_const a) + E) ") (#) (seq_const a)) . n <= (seq_const b) . n
A12: ((((seq_const a) + E) ") (#) (seq_const a)) . n = ((((seq_const a) + E) ") . n) * ((seq_const a) . n) by SEQ_1:8
.= ((((seq_const a) + E) . n) ") * ((seq_const a) . n) by VALUED_1:10
.= ((((seq_const a) . n) + (E . n)) ") * ((seq_const a) . n) by SEQ_1:7
.= ((((seq_const a) . n) + (1 / (n + 1))) ") * ((seq_const a) . n) by A3
.= ((a + (1 / (n + 1))) ") * ((seq_const a) . n) by SEQ_1:57
.= ((a + (1 / (n + 1))) ") * a by SEQ_1:57 ;
(seq_const b) . n = b by SEQ_1:57;
hence ((((seq_const a) + E) ") (#) (seq_const a)) . n <= (seq_const b) . n by A12, A1; :: thesis: verum

end;

then lim ((((seq_const a) + E) ") (#) (seq_const a)) <= lim (seq_const b) by SEQ_2:18, A9;
hence 1 <= b by A11, A2P, SEQ_4:25; :: thesis: verum