let g be Real; :: thesis: for f being PartFunc of REAL,REAL st ( for h being non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant 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 constant 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();

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

let n be 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 :: thesis: a . n <> 0

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 A6;
hence a . n <> 0 by SEQ_1:5; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

then A8: a is non-zero by SEQ_1:5;
A9: lim h1 = 0 ;
A10: lim h2 = 0 ;
A11: a is convergent by A6, A9, A10, Th1;
lim a = 0 by A6, A9, A10, Th1;
then reconsider a = a as non-zero 0 -convergent Real_Sequence by A11, A8, FDIFF_1:def 1;
A12: rng (a + c) c= dom f

proof

let x be object ; :: 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
A13: x = (a + c) . n by FUNCT_2:113;
consider m being Element of NAT such that
A14: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

now :: thesis: (a + c) . n in dom f

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

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

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

end;

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

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

end;

end;

end;

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

end;

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

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

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:15
.= ((a ") (#) ((f /* (a + c)) - (f /* c))) . ((2 * n) + 1) by A20
.= ((a ") . ((2 * n) + 1)) * (((f /* (a + c)) - (f /* c)) . ((2 * n) + 1)) by SEQ_1:8
.= ((a ") . ((2 * n) + 1)) * (((f /* (a + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1))) by RFUNCT_2:1
.= ((a ") . ((2 * n) + 1)) * ((f . ((a + c) . ((2 * n) + 1))) - ((f /* c) . ((2 * n) + 1))) by A12, FUNCT_2:108
.= ((a ") . ((2 * n) + 1)) * ((f . ((a . ((2 * n) + 1)) + (c . ((2 * n) + 1)))) - ((f /* c) . ((2 * n) + 1))) by SEQ_1:7
.= ((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:7
.= ((a ") . ((2 * n) + 1)) * (((f /* (h2 + c)) . n) - ((f /* c) . ((2 * n) + 1))) by A4, FUNCT_2:108
.= ((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:108
.= ((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: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;

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

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

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:15
.= ((a ") (#) ((f /* (a + c)) - (f /* c))) . (2 * n) by A23
.= ((a ") . (2 * n)) * (((f /* (a + c)) - (f /* c)) . (2 * n)) by SEQ_1:8
.= ((a ") . (2 * n)) * (((f /* (a + c)) . (2 * n)) - ((f /* c) . (2 * n))) by RFUNCT_2:1
.= ((a ") . (2 * n)) * ((f . ((a + c) . (2 * n))) - ((f /* c) . (2 * n))) by A12, FUNCT_2:108
.= ((a ") . (2 * n)) * ((f . ((a . (2 * n)) + (c . (2 * n)))) - ((f /* c) . (2 * n))) by SEQ_1:7
.= ((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:7
.= ((a ") . (2 * n)) * (((f /* (h1 + c)) . n) - ((f /* c) . (2 * n))) by A3, FUNCT_2:108
.= ((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:108
.= ((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: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;

then A24: ((a ") (#) ((f /* (a + c)) - (f /* c))) * I1 = (h1 ") (#) ((f /* (h1 + c)) - (f /* c)) ;
((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 A19, A22, A24, A21, SEQ_4:17; :: thesis: verum