let g be Real; :: thesis: for f being PartFunc of REAL ,REAL st ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {g} & rng (h + c) c= dom f & {g} c= dom f holds
(h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent ) holds
for h1, h2 being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {g} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & {g} c= dom f holds
lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c)))
let f be PartFunc of REAL ,REAL ; :: thesis: ( ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {g} & rng (h + c) c= dom f & {g} c= dom f holds
(h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent ) implies for h1, h2 being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {g} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & {g} c= dom f holds
lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c))) )
assume A1: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {g} & rng (h + c) c= dom f & {g} c= dom f holds
(h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent ; :: thesis: for h1, h2 being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {g} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & {g} c= dom f holds
lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c)))
let h1, h2 be convergent_to_0 Real_Sequence; :: thesis: for c being V8() Real_Sequence st rng c = {g} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & {g} c= dom f holds
lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c)))
let c be V8() Real_Sequence; :: thesis: ( rng c = {g} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & {g} c= dom f implies lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c))) )
assume that
A2: rng c = {g} and
A3: rng (h1 + c) c= dom f and
A4: rng (h2 + c) c= dom f and
A5: {g} c= dom f ; :: thesis: lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c)))
deffunc H₁( Element of NAT ) -> Element of REAL = h2 . $1;
deffunc H₂( Element of NAT ) -> Element of REAL = h1 . $1;
consider a being Real_Sequence such that
A6: for n being Element of NAT holds
( a . (2 * n) = H₂(n) & a . ((2 * n) + 1) = H₁(n) ) from SCHEME1:sch 2();
A7: h2 is non-empty by FDIFF_1:def 1;
A8: h1 is non-empty by FDIFF_1:def 1;

now

let n be Element of NAT ; :: thesis: a . n <> 0
consider m being Element of NAT such that
A9: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

now

per cases ( n = 2 * m or n = (2 * m) + 1 ) by A9;

suppose n = 2 * m ; :: thesis: a . n <> 0

then a . n = h1 . m by A6;
hence a . n <> 0 by A8, SEQ_1:7; :: thesis: verum

end;

suppose n = (2 * m) + 1 ; :: thesis: a . n <> 0

then a . n = h2 . m by A6;
hence a . n <> 0 by A7, SEQ_1:7; :: thesis: verum

end;

end;

end;

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

end;

then A10: a is non-empty by SEQ_1:7;
A11: lim h1 = 0 by FDIFF_1:def 1;
A12: lim h2 = 0 by FDIFF_1:def 1;
A13: h2 is convergent by FDIFF_1:def 1;
A14: h1 is convergent by FDIFF_1:def 1;
then A15: a is convergent by A6, A11, A13, A12, Th1;
lim a = 0 by A6, A14, A11, A13, A12, Th1;
then reconsider a = a as convergent_to_0 Real_Sequence by A15, A10, FDIFF_1:def 1;
A16: rng (a + c) c= dom f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (a + c) or x in dom f )
assume x in rng (a + c) ; :: thesis: x in dom f
then consider n being Element of NAT such that
A17: x = (a + c) . n by FUNCT_2:190;
consider m being Element of NAT such that
A18: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

now

per cases ( n = 2 * m or n = (2 * m) + 1 ) by A18;

suppose A19: n = 2 * m ; :: thesis: (a + c) . n in dom f

A20: (h1 + c) . m in rng (h1 + c) by VALUED_0:28;
(a + c) . n = (a . n) + (c . n) by SEQ_1:11
.= (h1 . m) + (c . n) by A6, A19
.= (h1 . m) + (c . m) by VALUED_0:23
.= (h1 + c) . m by SEQ_1:11 ;
hence (a + c) . n in dom f by A3, A20; :: thesis: verum

end;

suppose A21: n = (2 * m) + 1 ; :: thesis: (a + c) . n in dom f

A22: (h2 + c) . m in rng (h2 + c) by VALUED_0:28;
(a + c) . n = (a . n) + (c . n) by SEQ_1:11
.= (h2 . m) + (c . n) by A6, A21
.= (h2 . m) + (c . m) by VALUED_0:23
.= (h2 + c) . m by SEQ_1:11 ;
hence (a + c) . n in dom f by A4, A22; :: thesis: verum

end;

end;

end;

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

end;

then A23: (a " ) (#) ((f /* (a + c)) - (f /* c)) is convergent by A1, A2, A5;
deffunc H₃( Element of NAT ) -> Element of NAT = (2 * $1) + 1;
consider d being Real_Sequence such that
A24: for n being Element of NAT holds d . n = H₃(n) from SEQ_1:sch 1();
reconsider I2 = d as V36() sequence of NAT by A24, Th3;

now

let n be Element of NAT ; :: thesis: (((a " ) (#) ((f /* (a + c)) - (f /* c))) * I2) . n = ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c))) . n
thus (((a " ) (#) ((f /* (a + c)) - (f /* c))) * I2) . n = ((a " ) (#) ((f /* (a + c)) - (f /* c))) . (I2 . n) by FUNCT_2:21
.= ((a " ) (#) ((f /* (a + c)) - (f /* c))) . ((2 * n) + 1) by A24
.= ((a " ) . ((2 * n) + 1)) * (((f /* (a + c)) - (f /* c)) . ((2 * n) + 1)) by SEQ_1:12
.= ((a " ) . ((2 * n) + 1)) * (((f /* (a + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1))) by RFUNCT_2:6
.= ((a " ) . ((2 * n) + 1)) * ((f . ((a + c) . ((2 * n) + 1))) - ((f /* c) . ((2 * n) + 1))) by A16, FUNCT_2:185
.= ((a " ) . ((2 * n) + 1)) * ((f . ((a . ((2 * n) + 1)) + (c . ((2 * n) + 1)))) - ((f /* c) . ((2 * n) + 1))) by SEQ_1:11
.= ((a " ) . ((2 * n) + 1)) * ((f . ((h2 . n) + (c . ((2 * n) + 1)))) - ((f /* c) . ((2 * n) + 1))) by A6
.= ((a " ) . ((2 * n) + 1)) * ((f . ((h2 . n) + (c . n))) - ((f /* c) . ((2 * n) + 1))) by VALUED_0:23
.= ((a " ) . ((2 * n) + 1)) * ((f . ((h2 + c) . n)) - ((f /* c) . ((2 * n) + 1))) by SEQ_1:11
.= ((a " ) . ((2 * n) + 1)) * (((f /* (h2 + c)) . n) - ((f /* c) . ((2 * n) + 1))) by A4, FUNCT_2:185
.= ((a . ((2 * n) + 1)) " ) * (((f /* (h2 + c)) . n) - ((f /* c) . ((2 * n) + 1))) by VALUED_1:10
.= ((h2 . n) " ) * (((f /* (h2 + c)) . n) - ((f /* c) . ((2 * n) + 1))) by A6
.= ((h2 " ) . n) * (((f /* (h2 + c)) . n) - ((f /* c) . ((2 * n) + 1))) by VALUED_1:10
.= ((h2 " ) . n) * (((f /* (h2 + c)) . n) - (f . (c . ((2 * n) + 1)))) by A2, A5, FUNCT_2:185
.= ((h2 " ) . n) * (((f /* (h2 + c)) . n) - (f . (c . n))) by VALUED_0:23
.= ((h2 " ) . n) * (((f /* (h2 + c)) . n) - ((f /* c) . n)) by A2, A5, FUNCT_2:185
.= ((h2 " ) . n) * (((f /* (h2 + c)) - (f /* c)) . n) by RFUNCT_2:6
.= ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c))) . n by SEQ_1:12 ; :: thesis: verum

end;

then A25: ((a " ) (#) ((f /* (a + c)) - (f /* c))) * I2 = (h2 " ) (#) ((f /* (h2 + c)) - (f /* c)) by FUNCT_2:113;
((a " ) (#) ((f /* (a + c)) - (f /* c))) * I2 is subsequence of (a " ) (#) ((f /* (a + c)) - (f /* c)) by VALUED_0:def 17;
then A26: lim (((a " ) (#) ((f /* (a + c)) - (f /* c))) * I2) = lim ((a " ) (#) ((f /* (a + c)) - (f /* c))) by A23, SEQ_4:30;
deffunc H₄( Element of NAT ) -> Element of NAT = 2 * $1;
consider b being Real_Sequence such that
A27: for n being Element of NAT holds b . n = H₄(n) from SEQ_1:sch 1();
reconsider I1 = b as V36() sequence of NAT by A27, Th2;

now

let n be Element of NAT ; :: thesis: (((a " ) (#) ((f /* (a + c)) - (f /* c))) * I1) . n = ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) . n
thus (((a " ) (#) ((f /* (a + c)) - (f /* c))) * I1) . n = ((a " ) (#) ((f /* (a + c)) - (f /* c))) . (I1 . n) by FUNCT_2:21
.= ((a " ) (#) ((f /* (a + c)) - (f /* c))) . (2 * n) by A27
.= ((a " ) . (2 * n)) * (((f /* (a + c)) - (f /* c)) . (2 * n)) by SEQ_1:12
.= ((a " ) . (2 * n)) * (((f /* (a + c)) . (2 * n)) - ((f /* c) . (2 * n))) by RFUNCT_2:6
.= ((a " ) . (2 * n)) * ((f . ((a + c) . (2 * n))) - ((f /* c) . (2 * n))) by A16, FUNCT_2:185
.= ((a " ) . (2 * n)) * ((f . ((a . (2 * n)) + (c . (2 * n)))) - ((f /* c) . (2 * n))) by SEQ_1:11
.= ((a " ) . (2 * n)) * ((f . ((h1 . n) + (c . (2 * n)))) - ((f /* c) . (2 * n))) by A6
.= ((a " ) . (2 * n)) * ((f . ((h1 . n) + (c . n))) - ((f /* c) . (2 * n))) by VALUED_0:23
.= ((a " ) . (2 * n)) * ((f . ((h1 + c) . n)) - ((f /* c) . (2 * n))) by SEQ_1:11
.= ((a " ) . (2 * n)) * (((f /* (h1 + c)) . n) - ((f /* c) . (2 * n))) by A3, FUNCT_2:185
.= ((a . (2 * n)) " ) * (((f /* (h1 + c)) . n) - ((f /* c) . (2 * n))) by VALUED_1:10
.= ((h1 . n) " ) * (((f /* (h1 + c)) . n) - ((f /* c) . (2 * n))) by A6
.= ((h1 " ) . n) * (((f /* (h1 + c)) . n) - ((f /* c) . (2 * n))) by VALUED_1:10
.= ((h1 " ) . n) * (((f /* (h1 + c)) . n) - (f . (c . (2 * n)))) by A2, A5, FUNCT_2:185
.= ((h1 " ) . n) * (((f /* (h1 + c)) . n) - (f . (c . n))) by VALUED_0:23
.= ((h1 " ) . n) * (((f /* (h1 + c)) . n) - ((f /* c) . n)) by A2, A5, FUNCT_2:185
.= ((h1 " ) . n) * (((f /* (h1 + c)) - (f /* c)) . n) by RFUNCT_2:6
.= ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) . n by SEQ_1:12 ; :: thesis: verum

end;

then A28: ((a " ) (#) ((f /* (a + c)) - (f /* c))) * I1 = (h1 " ) (#) ((f /* (h1 + c)) - (f /* c)) by FUNCT_2:113;
((a " ) (#) ((f /* (a + c)) - (f /* c))) * I1 is subsequence of (a " ) (#) ((f /* (a + c)) - (f /* c)) by VALUED_0:def 17;
hence lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c))) by A23, A26, A28, A25, SEQ_4:30; :: thesis: verum