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 H1( Element of NAT ) -> Element of REAL = h2 . $1;
deffunc H2( 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) = H2(n) & d . ((2 * n) + 1) = H1(n) ) from SCHEME1:sch 2();
now :: thesis: for n being Nat holds d . n <> 0
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;
now :: thesis: d . n <> 0
per cases ( n = 2 * m or n = (2 * m) + 1 ) by A9;
suppose A10: n = 2 * m ; :: thesis: d . n <> 0
d . (2 * m) = h1 . m by A8;
hence d . n <> 0 by A10, SEQ_1:5; :: thesis: verum
end;
suppose A11: n = (2 * m) + 1 ; :: thesis: d . n <> 0
d . ((2 * m) + 1) = h2 . m by A8;
hence d . n <> 0 by A11, SEQ_1:5; :: thesis: verum
end;
end;
end;
hence d . n <> 0 ; :: thesis: verum
end;
then A12: d is non-zero by SEQ_1:5;
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 H3( Nat) -> set = 2 * $1;
consider a being Real_Sequence such that
A14: for n being Nat holds a . n = H3(n) from SEQ_1:sch 1();
 deffunc H4( Nat) -> Element of NAT = (2 * $1) + 1;
consider b being Real_Sequence such that
A15: for n being Nat holds b . n = H4(n) from SEQ_1:sch 1();
 for n being Element of NAT holds b . n = H4(n) by A15;
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;
now :: thesis: x in dom f
per cases ( n = 2 * m or n = (2 * m) + 1 ) by A18;
suppose n = 2 * m ; :: thesis: x in dom f
then x = (h1 . m) + (c . (2 * m)) by A8, A19
.= (h1 . m) + (c . m) by VALUED_0:23
.= (h1 + c) . m by SEQ_1:7 ;
then x in rng (h1 + c) by VALUED_0:28;
hence x in dom f by A4; :: thesis: verum
end;
suppose n = (2 * m) + 1 ; :: thesis: x in dom f
then x = (h2 . m) + (c . ((2 * m) + 1)) by A8, A19
.= (h2 . m) + (c . m) by VALUED_0:23
.= (h2 + c) . m by SEQ_1:7 ;
then x in rng (h2 + c) by VALUED_0:28;
hence x in dom f by A6; :: thesis: verum
end;
end;
end;
hence x in dom f ; :: thesis: verum
end;
now :: thesis: for n being Element of NAT holds (((d ") (#) ((f /* (d + c)) - (f /* c))) * b) . n = ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n
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;
then A20: (h2 ") (#) ((f /* (h2 + c)) - (f /* c)) is subsequence of (d ") (#) ((f /* (d + c)) - (f /* c)) by FUNCT_2:63;
now :: thesis: for n being Nat holds d . n < 0
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;
now :: thesis: d . n < 0
per cases ( n = 2 * m or n = (2 * m) + 1 ) by A21;
suppose A22: n = 2 * m ; :: thesis: d . n < 0
d . (2 * m) = h1 . m by A8;
hence d . n < 0 by A5, A22; :: thesis: verum
end;
suppose A23: n = (2 * m) + 1 ; :: thesis: d . n < 0
d . ((2 * m) + 1) = h2 . m by A8;
hence d . n < 0 by A7, A23; :: thesis: verum
end;
end;
end;
hence d . n < 0 ; :: thesis: verum
end;
then A24: (d ") (#) ((f /* (d + c)) - (f /* c)) is convergent by A1, A3, A16;
for n being Element of NAT holds a . n = H3(n) by A14;
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
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;
then (h1 ") (#) ((f /* (h1 + c)) - (f /* c)) is subsequence of (d ") (#) ((f /* (d + c)) - (f /* c)) by FUNCT_2:63;
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