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 & rng (h2 + c) c= dom f & ( for n being Element of NAT holds h1 . n > 0 ) & ( 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 & rng (h2 + c) c= dom f & ( for n being Element of NAT holds h1 . n > 0 ) & ( 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 & rng (h2 + c) c= dom f & ( for n being Element of NAT holds h1 . n > 0 ) & ( 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 & rng (h2 + c) c= dom f & ( for n being Element of NAT holds h1 . n > 0 ) & ( 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 & rng (h2 + c) c= dom f & ( for n being Element of NAT holds h1 . n > 0 ) & ( 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 & rng (h2 + c) c= dom f & ( for n being Element of NAT holds h1 . n > 0 ) & ( 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 H1( Element of NAT ) -> Element of REAL = h1 . $1;
deffunc H2( 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) = H1(n) & d . ((2 * n) + 1) = H2(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;
d is non-zero
proof
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 n = 2 * m ; :: thesis: d . n <> 0
then d . n = h1 . m by A3;
hence d . n <> 0 by A4, SEQ_1:7; :: thesis: verum
end;
suppose n = (2 * m) + 1 ; :: thesis: d . n <> 0
then d . n = h2 . m by A3;
hence d . n <> 0 by A5, SEQ_1:7; :: thesis: verum
end;
end;
end;
hence d . n <> 0 ; :: thesis: verum
end;
hence d is non-zero by SEQ_1:7; :: thesis: verum
end;
then reconsider d = d as convergent_to_0 Real_Sequence by A6, FDIFF_1:def 1;
A8: 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
A9: x = (d + 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 n = 2 * m ; :: thesis: x in dom f
then x = (d . (2 * m)) + (c . (2 * m)) by A9, SEQ_1:11
.= (h1 . m) + (c . (2 * m)) by A3
.= (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 = (d . ((2 * m) + 1)) + (c . ((2 * m) + 1)) by A9, SEQ_1:11
.= (h2 . m) + (c . ((2 * m) + 1)) by A3
.= (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;
for n being Element of NAT holds d . n > 0
proof
let n be Element of NAT ; :: thesis: d . n > 0
consider m being Element of NAT such that
A11: ( n = 2 * m or n = (2 * m) + 1 ) by SCHEME1:1;
now
per cases ( n = 2 * m or n = (2 * m) + 1 ) by A11;
suppose n = 2 * m ; :: thesis: d . n > 0
then d . n = h1 . m by A3;
hence d . n > 0 by A2; :: thesis: verum
end;
suppose n = (2 * m) + 1 ; :: thesis: d . n > 0
then d . n = h2 . m by A3;
hence d . n > 0 by A2; :: thesis: verum
end;
end;
end;
hence d . n > 0 ; :: thesis: verum
end;
then A12: (d " ) (#) ((f /* (d + c)) - (f /* c)) is convergent by A1, A2, A8;
deffunc H3( Element of NAT ) -> Element of NAT = 2 * $1;
consider a being Real_Sequence such that
A13: for n being Element of NAT holds a . n = H3(n) from SEQ_1:sch 1();
 reconsider a = a as V32 sequence of NAT by A13, FDIFF_2:2;
deffunc H4( Element of NAT ) -> Element of NAT = (2 * $1) + 1;
consider b being Real_Sequence such that
A14: for n being Element of NAT holds b . n = H4(n) from SEQ_1:sch 1();
 reconsider b = b as V32 sequence of NAT by A14, FDIFF_2:3;
A15: ((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 A13
.= ((d " ) . (2 * n)) * (((f /* (d + c)) - (f /* c)) . (2 * n)) by SEQ_1:12
.= ((d . (2 * n)) " ) * (((f /* (d + c)) - (f /* c)) . (2 * n)) by VALUED_1:10
.= ((h1 . n) " ) * (((f /* (d + c)) - (f /* c)) . (2 * n)) by A3
.= ((h1 " ) . n) * (((f /* (d + c)) - (f /* c)) . (2 * n)) by VALUED_1:10
.= ((h1 " ) . n) * (((f /* (d + c)) . (2 * n)) - ((f /* c) . (2 * n))) by RFUNCT_2:6
.= ((h1 " ) . n) * ((f . ((d + c) . (2 * n))) - ((f /* c) . (2 * n))) by A8, FUNCT_2:185
.= ((h1 " ) . n) * ((f . ((d + c) . (2 * n))) - (f . (c . (2 * n)))) by A1, A2, 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 . (2 * n)))) - (f . (c . n))) by VALUED_0:23
.= ((h1 " ) . n) * ((f . ((h1 . n) + (c . n))) - (f . (c . n))) by VALUED_0:23
.= ((h1 " ) . n) * ((f . ((h1 + c) . n)) - (f . (c . n))) by SEQ_1:11
.= ((h1 " ) . n) * (((f /* (h1 + c)) . n) - (f . (c . n))) by A2, FUNCT_2:185
.= ((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;
A16: ((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 A14
.= ((d " ) . ((2 * n) + 1)) * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by SEQ_1:12
.= ((d . ((2 * n) + 1)) " ) * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by VALUED_1:10
.= ((h2 . n) " ) * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by A3
.= ((h2 " ) . n) * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1)) by VALUED_1:10
.= ((h2 " ) . n) * (((f /* (d + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1))) by RFUNCT_2:6
.= ((h2 " ) . n) * ((f . ((d + c) . ((2 * n) + 1))) - ((f /* c) . ((2 * n) + 1))) by A8, FUNCT_2:185
.= ((h2 " ) . n) * ((f . ((d + c) . ((2 * n) + 1))) - (f . (c . ((2 * n) + 1)))) by A1, A2, 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 . ((2 * n) + 1)))) - (f . (c . n))) by VALUED_0:23
.= ((h2 " ) . n) * ((f . ((h2 . n) + (c . n))) - (f . (c . n))) by VALUED_0:23
.= ((h2 " ) . n) * ((f . ((h2 + c) . n)) - (f . (c . n))) by SEQ_1:11
.= ((h2 " ) . n) * (((f /* (h2 + c)) . n) - (f . (c . n))) by A2, FUNCT_2:185
.= ((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;
A17: (h1 " ) (#) ((f /* (h1 + c)) - (f /* c)) is subsequence of (d " ) (#) ((f /* (d + c)) - (f /* c)) by A15;
A18: (h2 " ) (#) ((f /* (h2 + c)) - (f /* c)) is subsequence of (d " ) (#) ((f /* (d + c)) - (f /* c)) by A16;
lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) = lim ((d " ) (#) ((f /* (d + c)) - (f /* c))) by A12, A17, SEQ_4:30;
hence lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c))) by A12, A18, SEQ_4:30; :: thesis: verum