let f be PartFunc of REAL,REAL; 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 & ( for n being Nat holds h1 . n < 0 ) & rng (h2 + c) c= dom f & ( 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; ( ( 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 & ( for n being Nat holds h1 . n < 0 ) & rng (h2 + c) c= dom f & ( 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
; 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 & ( for n being Nat holds h1 . n < 0 ) & rng (h2 + c) c= dom f & ( 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; for c being constant Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & ( for n being Nat holds h1 . n < 0 ) & rng (h2 + c) c= dom f & ( 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; ( rng c = {x0} & rng (h1 + c) c= dom f & ( for n being Nat holds h1 . n < 0 ) & rng (h2 + c) c= dom f & ( 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:
for n being Nat holds h1 . n < 0
and
A6:
rng (h2 + c) c= dom f
and
A7:
for n being Nat holds h2 . n < 0
; lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))
deffunc H1( Element of NAT ) -> Element of REAL = h2 . $1;
deffunc H2( 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) = H2(n) & d . ((2 * n) + 1) = H1(n) )
from SCHEME1:sch 2();
then A12:
d is non-zero
by SEQ_1:5;
A13:
( h2 is convergent & lim h2 = 0 )
;
( h1 is convergent & lim h1 = 0 )
;
then
( d is convergent & lim d = 0 )
by A8, A13, FDIFF_2:1;
then reconsider d = d as non-zero 0 -convergent Real_Sequence by A12, FDIFF_1:def 1;
deffunc H3( Nat) -> set = 2 * $1;
consider a being Real_Sequence such that
A14:
for n being Nat holds a . n = H3(n)
from SEQ_1:sch 1();
deffunc H4( Nat) -> Element of NAT = (2 * $1) + 1;
consider b being Real_Sequence such that
A15:
for n being Nat holds b . n = H4(n)
from SEQ_1:sch 1();
for n being Element of NAT holds b . n = H4(n)
by A15;
then reconsider b = b as V45() sequence of NAT by FDIFF_2:3;
A16:
rng (d + c) c= dom f
then A20:
(h2 ") (#) ((f /* (h2 + c)) - (f /* c)) is subsequence of (d ") (#) ((f /* (d + c)) - (f /* c))
by FUNCT_2:63;
then A24:
(d ") (#) ((f /* (d + c)) - (f /* c)) is convergent
by A1, A3, A16;
for n being Element of NAT holds a . n = H3(n)
by A14;
then reconsider a = a as V45() sequence of NAT by FDIFF_2:2;
then
(h1 ") (#) ((f /* (h1 + c)) - (f /* c)) is subsequence of (d ") (#) ((f /* (d + c)) - (f /* c))
by FUNCT_2:63;
then
lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((d ") (#) ((f /* (d + c)) - (f /* c)))
by A24, SEQ_4:17;
hence
lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))
by A24, A20, SEQ_4:17; verum