let f be PartFunc of REAL , REAL ; :: thesis: for x0 being Real st ( for h being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n < 0 ) holds
(h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent ) & {x0} c= dom f holds
for h1, h2 being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & ( for n being Element of NAT holds h1 . n < 0 ) & rng (h2 + c) c= dom f & ( for n being Element of 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 convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n < 0 ) holds
(h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent ) & {x0} c= dom f implies for h1, h2 being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & ( for n being Element of NAT holds h1 . n < 0 ) & rng (h2 + c) c= dom f & ( for n being Element of NAT holds h2 . n < 0 ) 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 V6 Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n < 0 ) holds
(h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent ) & {x0} c= dom f ) ; :: thesis: for h1, h2 being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & ( for n being Element of NAT holds h1 . n < 0 ) & rng (h2 + c) c= dom f & ( for n being Element of NAT holds h2 . n < 0 ) 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 V6 Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & ( for n being Element of NAT holds h1 . n < 0 ) & rng (h2 + c) c= dom f & ( for n being Element of NAT holds h2 . n < 0 ) holds
lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c)))
let c be V6 Real_Sequence; :: thesis: ( rng c = {x0} & rng (h1 + c) c= dom f & ( for n being Element of NAT holds h1 . n < 0 ) & rng (h2 + c) c= dom f & ( for n being Element of NAT holds h2 . n < 0 ) implies lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c))) )
assume A2: ( rng c = {x0} & rng (h1 + c) c= dom f & ( for n being Element of NAT holds h1 . n < 0 ) & rng (h2 + c) c= dom f & ( for n being Element of NAT holds h2 . n < 0 ) ) ; :: 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 d being Real_Sequence such that
A3: for n being Element of NAT holds
( d . (2 * n) = H₁(n) & d . ((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: ( d is convergent & lim d = 0 ) by A3, A4, FDIFF_2:1;

now

let n be Element of NAT ; :: thesis: d . 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 A8: n = 2 * m ; :: thesis: d . n <> 0

d . (2 * m) = h1 . m by A3;
hence d . n <> 0 by A4, A8, SEQ_1:7; :: thesis: verum

end;

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

d . ((2 * m) + 1) = h2 . m by A3;
hence d . n <> 0 by A5, A9, SEQ_1:7; :: thesis: verum

end;

end;

end;

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

end;

then d is non-zero by SEQ_1:7;
then reconsider d = d as convergent_to_0 Real_Sequence by A6, FDIFF_1:def 1;
A10: rng (d + c) c= dom f

proof

let x be set ; :: 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
A11: x = (d + c) . n by FUNCT_2:190;
A12: x = (d . n) + (c . n) by A11, SEQ_1:11;
consider m being Element of NAT such that
A13: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

now

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

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

then x = (h1 . m) + (c . (2 * m)) by A3, A12
.= (h1 . m) + (c . m) by VALUED_0:23
.= (h1 + c) . m by SEQ_1:11 ;
then x in rng (h1 + c) by VALUED_0:28;
hence x in dom f by A2; :: thesis: verum

end;

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

then x = (h2 . m) + (c . ((2 * m) + 1)) by A3, A12
.= (h2 . m) + (c . m) by VALUED_0:23
.= (h2 + c) . m by SEQ_1:11 ;
then x in rng (h2 + c) by VALUED_0:28;
hence x in dom f by A2; :: thesis: verum

end;

end;

end;

hence x in dom f ; :: thesis: verum

end;

now

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

now

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

suppose A15: n = 2 * m ; :: thesis: d . n < 0

d . (2 * m) = h1 . m by A3;
hence d . n < 0 by A2, A15; :: thesis: verum

end;

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

d . ((2 * m) + 1) = h2 . m by A3;
hence d . n < 0 by A2, A16; :: thesis: verum

end;

end;

end;

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

end;

then A17: (d " ) (#) ((f /* (d + c)) - (f /* c)) is convergent by A1, A2, A10;
deffunc H₃( Element of NAT ) -> Element of NAT = 2 * $1;
consider a being Real_Sequence such that
A18: for n being Element of NAT holds a . n = H₃(n) from SEQ_1:sch 1();
deffunc H₄( Element of NAT ) -> Element of NAT = (2 * $1) + 1;
consider b being Real_Sequence such that
A19: for n being Element of NAT holds b . n = H₄(n) from SEQ_1:sch 1();
reconsider a = a as V32 sequence of NAT by A18, FDIFF_2:2;
reconsider b = b as V32 sequence of NAT by A19, FDIFF_2:3;
A20: ((d " ) (#) ((f /* (d + c)) - (f /* c))) * a = (h1 " ) (#) ((f /* (h1 + c)) - (f /* c))

proof

now

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:21
.= ((d " ) (#) ((f /* (d + c)) - (f /* c))) . (2 * n) by A18
.= ((d " ) . (2 * n)) * (((f /* (d + c)) - (f /* c)) . (2 * n)) by SEQ_1:12
.= ((d " ) . (2 * n)) * (((f /* (d + c)) . (2 * n)) - ((f /* c) . (2 * n))) by RFUNCT_2:6
.= ((d . (2 * n)) " ) * (((f /* (d + c)) . (2 * n)) - ((f /* c) . (2 * n))) by VALUED_1:10
.= ((h1 . n) " ) * (((f /* (d + c)) . (2 * n)) - ((f /* c) . (2 * n))) by A3
.= ((h1 " ) . n) * (((f /* (d + c)) . (2 * n)) - ((f /* c) . (2 * n))) by VALUED_1:10
.= ((h1 " ) . n) * ((f . ((d + c) . (2 * n))) - ((f /* c) . (2 * n))) by A10, FUNCT_2:185
.= ((h1 " ) . n) * ((f . ((d . (2 * n)) + (c . (2 * n)))) - ((f /* c) . (2 * n))) by SEQ_1:11
.= ((h1 " ) . n) * ((f . ((h1 . n) + (c . (2 * n)))) - ((f /* c) . (2 * n))) by A3
.= ((h1 " ) . n) * ((f . ((h1 . n) + (c . n))) - ((f /* c) . (2 * n))) by VALUED_0:23
.= ((h1 " ) . n) * ((f . ((h1 + c) . n)) - ((f /* c) . (2 * n))) by SEQ_1:11
.= ((h1 " ) . n) * (((f /* (h1 + c)) . n) - ((f /* c) . (2 * n))) by A2, FUNCT_2:185
.= ((h1 " ) . n) * (((f /* (h1 + c)) . n) - (f . (c . (2 * n)))) by A1, 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 A1, 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 ((d " ) (#) ((f /* (d + c)) - (f /* c))) * a = (h1 " ) (#) ((f /* (h1 + c)) - (f /* c)) by FUNCT_2:113; :: thesis: verum

end;

A21: ((d " ) (#) ((f /* (d + c)) - (f /* c))) * b = (h2 " ) (#) ((f /* (h2 + c)) - (f /* c))

proof

now

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:21
.= ((d " ) (#) ((f /* (d + c)) - (f /* c))) . ((2 * n) + 1) by A19
.= ((d " ) . ((2 * n) + 1)) * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by SEQ_1:12
.= ((d " ) . ((2 * n) + 1)) * (((f /* (d + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1))) by RFUNCT_2:6
.= ((d . ((2 * n) + 1)) " ) * (((f /* (d + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1))) by VALUED_1:10
.= ((h2 . n) " ) * (((f /* (d + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1))) by A3
.= ((h2 " ) . n) * (((f /* (d + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1))) by VALUED_1:10
.= ((h2 " ) . n) * ((f . ((d + c) . ((2 * n) + 1))) - ((f /* c) . ((2 * n) + 1))) by A10, FUNCT_2:185
.= ((h2 " ) . n) * ((f . ((d . ((2 * n) + 1)) + (c . ((2 * n) + 1)))) - ((f /* c) . ((2 * n) + 1))) by SEQ_1:11
.= ((h2 " ) . n) * ((f . ((h2 . n) + (c . ((2 * n) + 1)))) - ((f /* c) . ((2 * n) + 1))) by A3
.= ((h2 " ) . n) * ((f . ((h2 . n) + (c . n))) - ((f /* c) . ((2 * n) + 1))) by VALUED_0:23
.= ((h2 " ) . n) * ((f . ((h2 + c) . n)) - ((f /* c) . ((2 * n) + 1))) by SEQ_1:11
.= ((h2 " ) . n) * (((f /* (h2 + c)) . n) - ((f /* c) . ((2 * n) + 1))) by A2, FUNCT_2:185
.= ((h2 " ) . n) * (((f /* (h2 + c)) . n) - (f . (c . ((2 * n) + 1)))) by A1, 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 A1, 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 ((d " ) (#) ((f /* (d + c)) - (f /* c))) * b = (h2 " ) (#) ((f /* (h2 + c)) - (f /* c)) by FUNCT_2:113; :: thesis: verum

end;

(h1 " ) (#) ((f /* (h1 + c)) - (f /* c)) is subsequence of (d " ) (#) ((f /* (d + c)) - (f /* c)) by A20;
then A22: lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) = lim ((d " ) (#) ((f /* (d + c)) - (f /* c))) by A17, SEQ_4:30;
(h2 " ) (#) ((f /* (h2 + c)) - (f /* c)) is subsequence of (d " ) (#) ((f /* (d + c)) - (f /* c)) by A21;
hence lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c))) by A17, A22, SEQ_4:30; :: thesis: verum