let f be PartFunc of REAL,REAL; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))

deffunc H_{1}( Element of NAT ) -> Element of REAL = h2 . $1;

deffunc H_{2}( 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) = H_{2}(n) & d . ((2 * n) + 1) = H_{1}(n) )
from SCHEME1:sch 2();

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 H_{3}( Nat) -> set = 2 * $1;

consider a being Real_Sequence such that

A14: for n being Nat holds a . n = H_{3}(n)
from SEQ_1:sch 1();

deffunc H_{4}( Nat) -> Element of NAT = (2 * $1) + 1;

consider b being Real_Sequence such that

A15: for n being Nat holds b . n = H_{4}(n)
from SEQ_1:sch 1();

for n being Element of NAT holds b . n = H_{4}(n)
by A15;

then reconsider b = b as V45() sequence of NAT by FDIFF_2:3;

A16: rng (d + c) c= dom f

for n being Element of NAT holds a . n = H_{3}(n)
by A14;

then reconsider a = a as V45() sequence of NAT by FDIFF_2:2;

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; :: thesis: verum

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; :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))

deffunc H

deffunc H

consider d being Real_Sequence such that

A8: for n being Element of NAT holds

( d . (2 * n) = H

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

then A12:
d is non-zero
by SEQ_1:5;let n be Nat; :: thesis: d . n <> 0

consider m being Element of NAT such that

A9: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

end;consider m being Element of NAT such that

A9: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

now :: thesis: d . n <> 0

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

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 H

consider a being Real_Sequence such that

A14: for n being Nat holds a . n = H

deffunc H

consider b being Real_Sequence such that

A15: for n being Nat holds b . n = H

for n being Element of NAT holds b . n = H

then reconsider b = b as V45() sequence of NAT by FDIFF_2:3;

A16: rng (d + c) c= dom f

proof

let x be object ; :: 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

A17: x = (d + c) . n by FUNCT_2:113;

consider m being Element of NAT such that

A18: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

A19: x = (d . n) + (c . n) by A17, SEQ_1:7;

end;assume x in rng (d + c) ; :: thesis: x in dom f

then consider n being Element of NAT such that

A17: x = (d + c) . n by FUNCT_2:113;

consider m being Element of NAT such that

A18: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

A19: x = (d . n) + (c . n) by A17, SEQ_1:7;

now :: thesis: x in dom f

hence
x in dom f
; :: thesis: verumend;

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

then A20:
(h2 ") (#) ((f /* (h2 + c)) - (f /* c)) is subsequence of (d ") (#) ((f /* (d + c)) - (f /* c))
by FUNCT_2:63;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:15

.= ((d ") (#) ((f /* (d + c)) - (f /* c))) . ((2 * n) + 1) by A15

.= ((d ") . ((2 * n) + 1)) * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by SEQ_1:8

.= ((d ") . ((2 * n) + 1)) * (((f /* (d + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1))) by RFUNCT_2:1

.= ((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 A8

.= ((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 A16, FUNCT_2:108

.= ((h2 ") . n) * ((f . ((d . ((2 * n) + 1)) + (c . ((2 * n) + 1)))) - ((f /* c) . ((2 * n) + 1))) by SEQ_1:7

.= ((h2 ") . n) * ((f . ((h2 . n) + (c . ((2 * n) + 1)))) - ((f /* c) . ((2 * n) + 1))) by A8

.= ((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:7

.= ((h2 ") . n) * (((f /* (h2 + c)) . n) - ((f /* c) . ((2 * n) + 1))) by A6, FUNCT_2:108

.= ((h2 ") . n) * (((f /* (h2 + c)) . n) - (f . (c . ((2 * n) + 1)))) by A2, A3, 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, A3, 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;thus (((d ") (#) ((f /* (d + c)) - (f /* c))) * b) . n = ((d ") (#) ((f /* (d + c)) - (f /* c))) . (b . n) by FUNCT_2:15

.= ((d ") (#) ((f /* (d + c)) - (f /* c))) . ((2 * n) + 1) by A15

.= ((d ") . ((2 * n) + 1)) * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by SEQ_1:8

.= ((d ") . ((2 * n) + 1)) * (((f /* (d + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1))) by RFUNCT_2:1

.= ((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 A8

.= ((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 A16, FUNCT_2:108

.= ((h2 ") . n) * ((f . ((d . ((2 * n) + 1)) + (c . ((2 * n) + 1)))) - ((f /* c) . ((2 * n) + 1))) by SEQ_1:7

.= ((h2 ") . n) * ((f . ((h2 . n) + (c . ((2 * n) + 1)))) - ((f /* c) . ((2 * n) + 1))) by A8

.= ((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:7

.= ((h2 ") . n) * (((f /* (h2 + c)) . n) - ((f /* c) . ((2 * n) + 1))) by A6, FUNCT_2:108

.= ((h2 ") . n) * (((f /* (h2 + c)) . n) - (f . (c . ((2 * n) + 1)))) by A2, A3, 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, A3, 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

now :: thesis: for n being Nat holds d . n < 0

then A24:
(d ") (#) ((f /* (d + c)) - (f /* c)) is convergent
by A1, A3, A16;let n be Nat; :: thesis: d . n < 0

consider m being Element of NAT such that

A21: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

end;consider m being Element of NAT such that

A21: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;

now :: thesis: d . n < 0

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

for n being Element of NAT holds a . n = H

then reconsider a = a as V45() sequence of NAT by FDIFF_2:2;

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

then
(h1 ") (#) ((f /* (h1 + c)) - (f /* c)) is subsequence of (d ") (#) ((f /* (d + c)) - (f /* c))
by FUNCT_2:63;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:15

.= ((d ") (#) ((f /* (d + c)) - (f /* c))) . (2 * n) by A14

.= ((d ") . (2 * n)) * (((f /* (d + c)) - (f /* c)) . (2 * n)) by SEQ_1:8

.= ((d ") . (2 * n)) * (((f /* (d + c)) . (2 * n)) - ((f /* c) . (2 * n))) by RFUNCT_2:1

.= ((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 A8

.= ((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 A16, FUNCT_2:108

.= ((h1 ") . n) * ((f . ((d . (2 * n)) + (c . (2 * n)))) - ((f /* c) . (2 * n))) by SEQ_1:7

.= ((h1 ") . n) * ((f . ((h1 . n) + (c . (2 * n)))) - ((f /* c) . (2 * n))) by A8

.= ((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:7

.= ((h1 ") . n) * (((f /* (h1 + c)) . n) - ((f /* c) . (2 * n))) by A4, FUNCT_2:108

.= ((h1 ") . n) * (((f /* (h1 + c)) . n) - (f . (c . (2 * n)))) by A2, A3, 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, A3, 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;thus (((d ") (#) ((f /* (d + c)) - (f /* c))) * a) . n = ((d ") (#) ((f /* (d + c)) - (f /* c))) . (a . n) by FUNCT_2:15

.= ((d ") (#) ((f /* (d + c)) - (f /* c))) . (2 * n) by A14

.= ((d ") . (2 * n)) * (((f /* (d + c)) - (f /* c)) . (2 * n)) by SEQ_1:8

.= ((d ") . (2 * n)) * (((f /* (d + c)) . (2 * n)) - ((f /* c) . (2 * n))) by RFUNCT_2:1

.= ((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 A8

.= ((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 A16, FUNCT_2:108

.= ((h1 ") . n) * ((f . ((d . (2 * n)) + (c . (2 * n)))) - ((f /* c) . (2 * n))) by SEQ_1:7

.= ((h1 ") . n) * ((f . ((h1 . n) + (c . (2 * n)))) - ((f /* c) . (2 * n))) by A8

.= ((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:7

.= ((h1 ") . n) * (((f /* (h1 + c)) . n) - ((f /* c) . (2 * n))) by A4, FUNCT_2:108

.= ((h1 ") . n) * (((f /* (h1 + c)) . n) - (f . (c . (2 * n)))) by A2, A3, 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, A3, 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

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; :: thesis: verum