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 A2: ( rng c = {g} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & {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 = h1 . $1;
deffunc H₂( Element of NAT ) -> Element of REAL = h2 . $1;
consider a being Real_Sequence such that
A3: for n being Element of NAT holds
( a . (2 * n) = H₁(n) & a . ((2 * n) + 1) = H₂(n) ) from SCHEME1:sch 2();
A4: ( h1 is convergent & lim h1 = 0 & h1 is non-zero ) by FDIFF_1:def 1;
A5: ( h2 is convergent & lim h2 = 0 & h2 is non-zero ) by FDIFF_1:def 1;
then A6: ( a is convergent & lim a = 0 ) by A3, A4, Th1;

now

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

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

then a is non-zero by SEQ_1:7;
then reconsider a = a as convergent_to_0 Real_Sequence by A6, FDIFF_1:def 1;
A8: 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
A9: x = (a + c) . n by FUNCT_2:190;
consider m being Element of NAT such that
A10: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

now

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

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

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

end;

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

A14: (a + c) . n = (a . n) + (c . n) by SEQ_1:11
.= (h2 . m) + (c . n) by A3, A13
.= (h2 . m) + (c . m) by VALUED_0:23
.= (h2 + c) . m by SEQ_1:11 ;
(h2 + c) . m in rng (h2 + c) by VALUED_0:28;
hence (a + c) . n in dom f by A2, A14; :: thesis: verum

end;

end;

end;

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

end;

then A15: (a " ) (#) ((f /* (a + c)) - (f /* c)) is convergent by A1, A2;
deffunc H₃( Element of NAT ) -> Element of NAT = 2 * $1;
deffunc H₄( Element of NAT ) -> Element of NAT = (2 * $1) + 1;
consider b being Real_Sequence such that
A16: for n being Element of NAT holds b . n = H₃(n) from SEQ_1:sch 1();
consider d being Real_Sequence such that
A17: for n being Element of NAT holds d . n = H₄(n) from SEQ_1:sch 1();
reconsider I1 = b as V35() sequence of NAT by A16, Th2;
reconsider I2 = d as V35() sequence of NAT by A17, Th3;
A18: ((a " ) (#) ((f /* (a + c)) - (f /* c))) * I1 is subsequence of (a " ) (#) ((f /* (a + c)) - (f /* c)) by VALUED_0:def 17;
((a " ) (#) ((f /* (a + c)) - (f /* c))) * I2 is subsequence of (a " ) (#) ((f /* (a + c)) - (f /* c)) by VALUED_0:def 17;
then A19: lim (((a " ) (#) ((f /* (a + c)) - (f /* c))) * I2) = lim ((a " ) (#) ((f /* (a + c)) - (f /* c))) by A15, SEQ_4:30;
A20: ((a " ) (#) ((f /* (a + c)) - (f /* c))) * I1 = (h1 " ) (#) ((f /* (h1 + c)) - (f /* c))

proof

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 A16
.= ((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 A8, 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 A3
.= ((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 A2, 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 A3
.= ((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, 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, 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;

hence ((a " ) (#) ((f /* (a + c)) - (f /* c))) * I1 = (h1 " ) (#) ((f /* (h1 + c)) - (f /* c)) by FUNCT_2:113; :: thesis: verum

end;

((a " ) (#) ((f /* (a + c)) - (f /* c))) * I2 = (h2 " ) (#) ((f /* (h2 + c)) - (f /* c))

proof

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 A17
.= ((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 A8, 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 A3
.= ((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 A2, 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 A3
.= ((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, 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, 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;

hence ((a " ) (#) ((f /* (a + c)) - (f /* c))) * I2 = (h2 " ) (#) ((f /* (h2 + c)) - (f /* c)) by FUNCT_2:113; :: thesis: verum

end;

hence lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c))) by A15, A18, A19, A20, SEQ_4:30; :: thesis: verum