let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) & {x0} c= dom f holds

for h1, h2 being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & ( for n being Nat holds h1 . n > 0 ) & ( for n being Nat holds h2 . n > 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))

let x0 be Real; :: thesis: ( ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) & {x0} c= dom f implies for h1, h2 being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & ( for n being Nat holds h1 . n > 0 ) & ( for n being Nat holds h2 . n > 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) )

assume that

A1: for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent and

A2: {x0} c= dom f ; :: thesis: for h1, h2 being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & ( for n being Nat holds h1 . n > 0 ) & ( for n being Nat holds h2 . n > 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))

let h1, h2 be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & ( for n being Nat holds h1 . n > 0 ) & ( for n being Nat holds h2 . n > 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))

let c be constant Real_Sequence; :: thesis: ( rng c = {x0} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & ( for n being Nat holds h1 . n > 0 ) & ( for n being Nat holds h2 . n > 0 ) implies lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) )

assume that

A3: rng c = {x0} and

A4: rng (h1 + c) c= dom f and

A5: rng (h2 + c) c= dom f and

A6: for n being Nat holds h1 . n > 0 and

A7: for n being Nat holds h2 . n > 0 ; :: thesis: lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))

deffunc H_{1}( Element of NAT ) -> Element of REAL = h2 . $1;

deffunc H_{2}( Element of NAT ) -> Element of REAL = h1 . $1;

consider d being Real_Sequence such that

A8: for n being Element of NAT holds

( d . (2 * n) = H_{2}(n) & d . ((2 * n) + 1) = H_{1}(n) )
from SCHEME1:sch 2();

A11: ( h2 is convergent & lim h2 = 0 ) ;

( h1 is convergent & lim h1 = 0 ) ;

then ( d is convergent & lim d = 0 ) by A8, A11, FDIFF_2:1;

then reconsider d = d as non-zero 0 -convergent Real_Sequence by A10, FDIFF_1:def 1;

deffunc H_{3}( Nat) -> set = 2 * $1;

consider a being Real_Sequence such that

A12: for n being Nat holds a . n = H_{3}(n)
from SEQ_1:sch 1();

deffunc H_{4}( Nat) -> Element of NAT = (2 * $1) + 1;

consider b being Real_Sequence such that

A13: for n being Nat holds b . n = H_{4}(n)
from SEQ_1:sch 1();

for n being Element of NAT holds b . n = H_{4}(n)
by A13;

then reconsider b = b as V45() sequence of NAT by FDIFF_2:3;

A14: rng (d + c) c= dom f

for n being Nat holds d . n > 0

for n being Element of NAT holds a . n = H_{3}(n)
by A12;

then reconsider a = a as V45() sequence of NAT by FDIFF_2:2;

then lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((d ") (#) ((f /* (d + c)) - (f /* c))) by A19, SEQ_4:17;

hence lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) by A19, A17, SEQ_4:17; :: thesis: verum

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) & {x0} c= dom f holds

for h1, h2 being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & ( for n being Nat holds h1 . n > 0 ) & ( for n being Nat holds h2 . n > 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))

let x0 be Real; :: thesis: ( ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) & {x0} c= dom f implies for h1, h2 being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & ( for n being Nat holds h1 . n > 0 ) & ( for n being Nat holds h2 . n > 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) )

assume that

A1: for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent and

A2: {x0} c= dom f ; :: thesis: for h1, h2 being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & ( for n being Nat holds h1 . n > 0 ) & ( for n being Nat holds h2 . n > 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))

let h1, h2 be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & ( for n being Nat holds h1 . n > 0 ) & ( for n being Nat holds h2 . n > 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))

let c be constant Real_Sequence; :: thesis: ( rng c = {x0} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & ( for n being Nat holds h1 . n > 0 ) & ( for n being Nat holds h2 . n > 0 ) implies lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) )

assume that

A3: rng c = {x0} and

A4: rng (h1 + c) c= dom f and

A5: rng (h2 + c) c= dom f and

A6: for n being Nat holds h1 . n > 0 and

A7: for n being Nat holds h2 . n > 0 ; :: thesis: lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))

deffunc H

deffunc H

consider d being Real_Sequence such that

A8: for n being Element of NAT holds

( d . (2 * n) = H

now :: thesis: for n being Nat holds d . n <> 0

then A10:
d is non-zero
by SEQ_1:5;let n be Nat; :: thesis: d . n <> 0

consider m being Element of NAT such that

A9: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

hence d . n <> 0 ; :: thesis: verum

end;consider m being Element of NAT such that

A9: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

hence d . n <> 0 ; :: thesis: verum

A11: ( h2 is convergent & lim h2 = 0 ) ;

( h1 is convergent & lim h1 = 0 ) ;

then ( d is convergent & lim d = 0 ) by A8, A11, FDIFF_2:1;

then reconsider d = d as non-zero 0 -convergent Real_Sequence by A10, FDIFF_1:def 1;

deffunc H

consider a being Real_Sequence such that

A12: for n being Nat holds a . n = H

deffunc H

consider b being Real_Sequence such that

A13: for n being Nat holds b . n = H

for n being Element of NAT holds b . n = H

then reconsider b = b as V45() sequence of NAT by FDIFF_2:3;

A14: rng (d + c) c= dom f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (d + c) or x in dom f )

assume x in rng (d + c) ; :: thesis: x in dom f

then consider n being Element of NAT such that

A15: x = (d + c) . n by FUNCT_2:113;

consider m being Element of NAT such that

A16: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

end;assume x in rng (d + c) ; :: thesis: x in dom f

then consider n being Element of NAT such that

A15: x = (d + c) . n by FUNCT_2:113;

consider m being Element of NAT such that

A16: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

now :: thesis: x in dom fend;

hence
x in dom f
; :: thesis: verumper cases
( n = 2 * m or n = (2 * m) + 1 )
by A16;

end;

suppose
n = 2 * m
; :: thesis: x in dom f

then x =
(d . (2 * m)) + (c . (2 * m))
by A15, SEQ_1:7

.= (h1 . m) + (c . (2 * m)) by A8

.= (h1 . m) + (c . m) by VALUED_0:23

.= (h1 + c) . m by SEQ_1:7 ;

then x in rng (h1 + c) by VALUED_0:28;

hence x in dom f by A4; :: thesis: verum

end;.= (h1 . m) + (c . (2 * m)) by A8

.= (h1 . m) + (c . m) by VALUED_0:23

.= (h1 + c) . m by SEQ_1:7 ;

then x in rng (h1 + c) by VALUED_0:28;

hence x in dom f by A4; :: thesis: verum

suppose
n = (2 * m) + 1
; :: thesis: x in dom f

then x =
(d . ((2 * m) + 1)) + (c . ((2 * m) + 1))
by A15, SEQ_1:7

.= (h2 . m) + (c . ((2 * m) + 1)) by A8

.= (h2 . m) + (c . m) by VALUED_0:23

.= (h2 + c) . m by SEQ_1:7 ;

then x in rng (h2 + c) by VALUED_0:28;

hence x in dom f by A5; :: thesis: verum

end;.= (h2 . m) + (c . ((2 * m) + 1)) by A8

.= (h2 . m) + (c . m) by VALUED_0:23

.= (h2 + c) . m by SEQ_1:7 ;

then x in rng (h2 + c) by VALUED_0:28;

hence x in dom f by A5; :: thesis: verum

now :: thesis: for n being Element of NAT holds (((d ") (#) ((f /* (d + c)) - (f /* c))) * b) . n = ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n

then A17:
(h2 ") (#) ((f /* (h2 + c)) - (f /* c)) is subsequence of (d ") (#) ((f /* (d + c)) - (f /* c))
by FUNCT_2:63;let n be Element of NAT ; :: thesis: (((d ") (#) ((f /* (d + c)) - (f /* c))) * b) . n = ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n

thus (((d ") (#) ((f /* (d + c)) - (f /* c))) * b) . n = ((d ") (#) ((f /* (d + c)) - (f /* c))) . (b . n) by FUNCT_2:15

.= ((d ") (#) ((f /* (d + c)) - (f /* c))) . ((2 * n) + 1) by A13

.= ((d ") . ((2 * n) + 1)) * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by SEQ_1:8

.= ((d . ((2 * n) + 1)) ") * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by VALUED_1:10

.= ((h2 . n) ") * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by A8

.= ((h2 ") . n) * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by VALUED_1:10

.= ((h2 ") . n) * (((f /* (d + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1))) by RFUNCT_2:1

.= ((h2 ") . n) * ((f . ((d + c) . ((2 * n) + 1))) - ((f /* c) . ((2 * n) + 1))) by A14, FUNCT_2:108

.= ((h2 ") . n) * ((f . ((d + c) . ((2 * n) + 1))) - (f . (c . ((2 * n) + 1)))) by A2, A3, FUNCT_2:108

.= ((h2 ") . n) * ((f . ((d . ((2 * n) + 1)) + (c . ((2 * n) + 1)))) - (f . (c . ((2 * n) + 1)))) by SEQ_1:7

.= ((h2 ") . n) * ((f . ((h2 . n) + (c . ((2 * n) + 1)))) - (f . (c . ((2 * n) + 1)))) by A8

.= ((h2 ") . n) * ((f . ((h2 . n) + (c . ((2 * n) + 1)))) - (f . (c . n))) by VALUED_0:23

.= ((h2 ") . n) * ((f . ((h2 . n) + (c . n))) - (f . (c . n))) by VALUED_0:23

.= ((h2 ") . n) * ((f . ((h2 + c) . n)) - (f . (c . n))) by SEQ_1:7

.= ((h2 ") . n) * (((f /* (h2 + c)) . n) - (f . (c . n))) by A5, FUNCT_2:108

.= ((h2 ") . n) * (((f /* (h2 + c)) . n) - ((f /* c) . n)) by A2, A3, FUNCT_2:108

.= ((h2 ") . n) * (((f /* (h2 + c)) - (f /* c)) . n) by RFUNCT_2:1

.= ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n by SEQ_1:8 ; :: thesis: verum

end;thus (((d ") (#) ((f /* (d + c)) - (f /* c))) * b) . n = ((d ") (#) ((f /* (d + c)) - (f /* c))) . (b . n) by FUNCT_2:15

.= ((d ") (#) ((f /* (d + c)) - (f /* c))) . ((2 * n) + 1) by A13

.= ((d ") . ((2 * n) + 1)) * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by SEQ_1:8

.= ((d . ((2 * n) + 1)) ") * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by VALUED_1:10

.= ((h2 . n) ") * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by A8

.= ((h2 ") . n) * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by VALUED_1:10

.= ((h2 ") . n) * (((f /* (d + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1))) by RFUNCT_2:1

.= ((h2 ") . n) * ((f . ((d + c) . ((2 * n) + 1))) - ((f /* c) . ((2 * n) + 1))) by A14, FUNCT_2:108

.= ((h2 ") . n) * ((f . ((d + c) . ((2 * n) + 1))) - (f . (c . ((2 * n) + 1)))) by A2, A3, FUNCT_2:108

.= ((h2 ") . n) * ((f . ((d . ((2 * n) + 1)) + (c . ((2 * n) + 1)))) - (f . (c . ((2 * n) + 1)))) by SEQ_1:7

.= ((h2 ") . n) * ((f . ((h2 . n) + (c . ((2 * n) + 1)))) - (f . (c . ((2 * n) + 1)))) by A8

.= ((h2 ") . n) * ((f . ((h2 . n) + (c . ((2 * n) + 1)))) - (f . (c . n))) by VALUED_0:23

.= ((h2 ") . n) * ((f . ((h2 . n) + (c . n))) - (f . (c . n))) by VALUED_0:23

.= ((h2 ") . n) * ((f . ((h2 + c) . n)) - (f . (c . n))) by SEQ_1:7

.= ((h2 ") . n) * (((f /* (h2 + c)) . n) - (f . (c . n))) by A5, FUNCT_2:108

.= ((h2 ") . n) * (((f /* (h2 + c)) . n) - ((f /* c) . n)) by A2, A3, FUNCT_2:108

.= ((h2 ") . n) * (((f /* (h2 + c)) - (f /* c)) . n) by RFUNCT_2:1

.= ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n by SEQ_1:8 ; :: thesis: verum

for n being Nat holds d . n > 0

proof

then A19:
(d ") (#) ((f /* (d + c)) - (f /* c)) is convergent
by A1, A3, A14;
let n be Nat; :: thesis: d . n > 0

consider m being Element of NAT such that

A18: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

hence d . n > 0 ; :: thesis: verum

end;consider m being Element of NAT such that

A18: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

hence d . n > 0 ; :: thesis: verum

for n being Element of NAT holds a . n = H

then reconsider a = a as V45() sequence of NAT by FDIFF_2:2;

now :: thesis: for n being Element of NAT holds (((d ") (#) ((f /* (d + c)) - (f /* c))) * a) . n = ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n

then
(h1 ") (#) ((f /* (h1 + c)) - (f /* c)) is subsequence of (d ") (#) ((f /* (d + c)) - (f /* c))
by FUNCT_2:63;let n be Element of NAT ; :: thesis: (((d ") (#) ((f /* (d + c)) - (f /* c))) * a) . n = ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n

thus (((d ") (#) ((f /* (d + c)) - (f /* c))) * a) . n = ((d ") (#) ((f /* (d + c)) - (f /* c))) . (a . n) by FUNCT_2:15

.= ((d ") (#) ((f /* (d + c)) - (f /* c))) . (2 * n) by A12

.= ((d ") . (2 * n)) * (((f /* (d + c)) - (f /* c)) . (2 * n)) by SEQ_1:8

.= ((d . (2 * n)) ") * (((f /* (d + c)) - (f /* c)) . (2 * n)) by VALUED_1:10

.= ((h1 . n) ") * (((f /* (d + c)) - (f /* c)) . (2 * n)) by A8

.= ((h1 ") . n) * (((f /* (d + c)) - (f /* c)) . (2 * n)) by VALUED_1:10

.= ((h1 ") . n) * (((f /* (d + c)) . (2 * n)) - ((f /* c) . (2 * n))) by RFUNCT_2:1

.= ((h1 ") . n) * ((f . ((d + c) . (2 * n))) - ((f /* c) . (2 * n))) by A14, FUNCT_2:108

.= ((h1 ") . n) * ((f . ((d + c) . (2 * n))) - (f . (c . (2 * n)))) by A2, A3, FUNCT_2:108

.= ((h1 ") . n) * ((f . ((d . (2 * n)) + (c . (2 * n)))) - (f . (c . (2 * n)))) by SEQ_1:7

.= ((h1 ") . n) * ((f . ((h1 . n) + (c . (2 * n)))) - (f . (c . (2 * n)))) by A8

.= ((h1 ") . n) * ((f . ((h1 . n) + (c . (2 * n)))) - (f . (c . n))) by VALUED_0:23

.= ((h1 ") . n) * ((f . ((h1 . n) + (c . n))) - (f . (c . n))) by VALUED_0:23

.= ((h1 ") . n) * ((f . ((h1 + c) . n)) - (f . (c . n))) by SEQ_1:7

.= ((h1 ") . n) * (((f /* (h1 + c)) . n) - (f . (c . n))) by A4, FUNCT_2:108

.= ((h1 ") . n) * (((f /* (h1 + c)) . n) - ((f /* c) . n)) by A2, A3, FUNCT_2:108

.= ((h1 ") . n) * (((f /* (h1 + c)) - (f /* c)) . n) by RFUNCT_2:1

.= ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n by SEQ_1:8 ; :: thesis: verum

end;thus (((d ") (#) ((f /* (d + c)) - (f /* c))) * a) . n = ((d ") (#) ((f /* (d + c)) - (f /* c))) . (a . n) by FUNCT_2:15

.= ((d ") (#) ((f /* (d + c)) - (f /* c))) . (2 * n) by A12

.= ((d ") . (2 * n)) * (((f /* (d + c)) - (f /* c)) . (2 * n)) by SEQ_1:8

.= ((d . (2 * n)) ") * (((f /* (d + c)) - (f /* c)) . (2 * n)) by VALUED_1:10

.= ((h1 . n) ") * (((f /* (d + c)) - (f /* c)) . (2 * n)) by A8

.= ((h1 ") . n) * (((f /* (d + c)) - (f /* c)) . (2 * n)) by VALUED_1:10

.= ((h1 ") . n) * (((f /* (d + c)) . (2 * n)) - ((f /* c) . (2 * n))) by RFUNCT_2:1

.= ((h1 ") . n) * ((f . ((d + c) . (2 * n))) - ((f /* c) . (2 * n))) by A14, FUNCT_2:108

.= ((h1 ") . n) * ((f . ((d + c) . (2 * n))) - (f . (c . (2 * n)))) by A2, A3, FUNCT_2:108

.= ((h1 ") . n) * ((f . ((d . (2 * n)) + (c . (2 * n)))) - (f . (c . (2 * n)))) by SEQ_1:7

.= ((h1 ") . n) * ((f . ((h1 . n) + (c . (2 * n)))) - (f . (c . (2 * n)))) by A8

.= ((h1 ") . n) * ((f . ((h1 . n) + (c . (2 * n)))) - (f . (c . n))) by VALUED_0:23

.= ((h1 ") . n) * ((f . ((h1 . n) + (c . n))) - (f . (c . n))) by VALUED_0:23

.= ((h1 ") . n) * ((f . ((h1 + c) . n)) - (f . (c . n))) by SEQ_1:7

.= ((h1 ") . n) * (((f /* (h1 + c)) . n) - (f . (c . n))) by A4, FUNCT_2:108

.= ((h1 ") . n) * (((f /* (h1 + c)) . n) - ((f /* c) . n)) by A2, A3, FUNCT_2:108

.= ((h1 ") . n) * (((f /* (h1 + c)) - (f /* c)) . n) by RFUNCT_2:1

.= ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n by SEQ_1:8 ; :: thesis: verum

then lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((d ") (#) ((f /* (d + c)) - (f /* c))) by A19, SEQ_4:17;

hence lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) by A19, A17, SEQ_4:17; :: thesis: verum