for a, b, d being Real_Sequence st a is convergent & b is convergent & lim a = lim b & ( for n being Nat holds
( d . (2 * n) = a . n & d . ((2 * n) + 1) = b . n ) ) holds
( d is convergent & lim d = lim a )

for a being Real_Sequence st ( for n being Nat holds a . n = 2 * n ) holds
( a is increasing & a is natural-yielding )

for a being Real_Sequence st ( for n being Nat holds a . n = (2 * n) + 1 ) holds
( a is increasing & a is natural-yielding )

for x0 being Real
for h being convergent_to_0 Real_Sequence
for c being constant Real_Sequence st rng c = {x0} holds
( c is convergent & lim c = x0 & h + c is convergent & lim (h + c) = x0 )

for r being Real
for a, b being Real_Sequence st rng a = {r} & rng b = {r} holds
a = b

for a being Real_Sequence
for h being convergent_to_0 Real_Sequence st a is subsequence of h holds
a is convergent_to_0 Real_Sequence

for g being Real
for f being PartFunc of REAL , REAL st ( for h being convergent_to_0 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 convergent_to_0 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)))

for r being Real
for f being PartFunc of REAL , REAL st ex N being Neighbourhood of r st N c= dom f holds
ex h being convergent_to_0 Real_Sequence ex c being constant Real_Sequence st
( rng c = {r} & rng (h + c) c= dom f & {r} c= dom f )

for a being Real_Sequence
for f2, f1 being PartFunc of REAL , REAL st rng a c= dom (f2 * f1) holds
( rng a c= dom f1 & rng (f1 * a) c= dom f2 )

for x0, r being Real
for f being PartFunc of REAL , REAL st f . x0 <> r & f is_differentiable_in x0 holds
ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) )

for x0 being Real
for f being PartFunc of REAL , REAL holds
( f is_differentiable_in x0 iff ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h " ) (#) ((f * (h + c)) - (f * c)) is convergent ) ) )

for x0, g being Real
for f being PartFunc of REAL , REAL holds
( f is_differentiable_in x0 & diff f,x0 = g iff ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
( (h " ) (#) ((f * (h + c)) - (f * c)) is convergent & lim ((h " ) (#) ((f * (h + c)) - (f * c))) = g ) ) ) )

for x0 being Real
for f1, f2 being PartFunc of REAL , REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in f1 . x0 holds
( f2 * f1 is_differentiable_in x0 & diff (f2 * f1),x0 = (diff f2,(f1 . x0)) * (diff f1,x0) )

for x0 being Real
for f2, f1 being PartFunc of REAL , REAL st f2 . x0 <> 0 & f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 / f2 is_differentiable_in x0 & diff (f1 / f2),x0 = (((diff f1,x0) * (f2 . x0)) - ((diff f2,x0) * (f1 . x0))) / ((f2 . x0) ^2 ) )

for x0 being Real
for f being PartFunc of REAL , REAL st f . x0 <> 0 & f is_differentiable_in x0 holds
( f ^ is_differentiable_in x0 & diff (f ^ ),x0 = - ((diff f,x0) / ((f . x0) ^2 )) )

for A being open Subset of REAL
for f being PartFunc of REAL , REAL st f is_differentiable_on A holds
( f | A is_differentiable_on A & f `| A = (f | A) `| A )

for A being open Subset of REAL
for f1, f2 being PartFunc of REAL , REAL st f1 is_differentiable_on A & f2 is_differentiable_on A holds
( f1 + f2 is_differentiable_on A & (f1 + f2) `| A = (f1 `| A) + (f2 `| A) )

for A being open Subset of REAL
for f1, f2 being PartFunc of REAL , REAL st f1 is_differentiable_on A & f2 is_differentiable_on A holds
( f1 - f2 is_differentiable_on A & (f1 - f2) `| A = (f1 `| A) - (f2 `| A) )

for r being Real
for A being open Subset of REAL
for f being PartFunc of REAL , REAL st f is_differentiable_on A holds
( r (#) f is_differentiable_on A & (r (#) f) `| A = r (#) (f `| A) )

for A being open Subset of REAL
for f1, f2 being PartFunc of REAL , REAL st f1 is_differentiable_on A & f2 is_differentiable_on A holds
( f1 (#) f2 is_differentiable_on A & (f1 (#) f2) `| A = ((f1 `| A) (#) f2) + (f1 (#) (f2 `| A)) )

for A being open Subset of REAL
for f1, f2 being PartFunc of REAL , REAL st f1 is_differentiable_on A & f2 is_differentiable_on A & ( for x0 being Real st x0 in A holds
f2 . x0 <> 0 ) holds
( f1 / f2 is_differentiable_on A & (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2) )

for A being open Subset of REAL
for f being PartFunc of REAL , REAL st f is_differentiable_on A & ( for x0 being Real st x0 in A holds
f . x0 <> 0 ) holds
( f ^ is_differentiable_on A & (f ^ ) `| A = - ((f `| A) / (f (#) f)) )

for A being open Subset of REAL
for f1, f2 being PartFunc of REAL , REAL st f1 is_differentiable_on A & f1 .: A is open Subset of REAL & f2 is_differentiable_on f1 .: A holds
( f2 * f1 is_differentiable_on A & (f2 * f1) `| A = ((f2 `| (f1 .: A)) * f1) (#) (f1 `| A) )

for A being open Subset of REAL
for f being PartFunc of REAL , REAL st A c= dom f & ( for r, p being Real st r in A & p in A holds
abs ((f . r) - (f . p)) <= (r - p) ^2 ) holds
( f is_differentiable_on A & ( for x0 being Real st x0 in A holds
diff f,x0 = 0 ) )

for p, g being Real
for f being PartFunc of REAL , REAL st ( for r1, r2 being Real st r1 in ].p,g.[ & r2 in ].p,g.[ holds
abs ((f . r1) - (f . r2)) <= (r1 - r2) ^2 ) & p < g & ].p,g.[ c= dom f holds
( f is_differentiable_on ].p,g.[ & f is_constant_on ].p,g.[ )

for r being Real
for f being PartFunc of REAL , REAL st left_open_halfline r c= dom f & ( for r1, r2 being Real st r1 in left_open_halfline r & r2 in left_open_halfline r holds
abs ((f . r1) - (f . r2)) <= (r1 - r2) ^2 ) holds
( f is_differentiable_on left_open_halfline r & f is_constant_on left_open_halfline r )

for r being Real
for f being PartFunc of REAL , REAL st right_open_halfline r c= dom f & ( for r1, r2 being Real st r1 in right_open_halfline r & r2 in right_open_halfline r holds
abs ((f . r1) - (f . r2)) <= (r1 - r2) ^2 ) holds
( f is_differentiable_on right_open_halfline r & f is_constant_on right_open_halfline r )

for f being PartFunc of REAL , REAL st f is total & ( for r1, r2 being Real holds abs ((f . r1) - (f . r2)) <= (r1 - r2) ^2 ) holds
( f is_differentiable_on [#] REAL & f is_constant_on [#] REAL )

for r being Real
for f being PartFunc of REAL , REAL st f is_differentiable_on left_open_halfline r & ( for x0 being Real st x0 in left_open_halfline r holds
0 < diff f,x0 ) holds
( f is_increasing_on left_open_halfline r & f | (left_open_halfline r) is one-to-one )

for r being Real
for f being PartFunc of REAL , REAL st f is_differentiable_on left_open_halfline r & ( for x0 being Real st x0 in left_open_halfline r holds
diff f,x0 < 0 ) holds
( f is_decreasing_on left_open_halfline r & f | (left_open_halfline r) is one-to-one )

for r being Real
for f being PartFunc of REAL , REAL st f is_differentiable_on left_open_halfline r & ( for x0 being Real st x0 in left_open_halfline r holds
0 <= diff f,x0 ) holds
f is_non_decreasing_on left_open_halfline r

for r being Real
for f being PartFunc of REAL , REAL st f is_differentiable_on left_open_halfline r & ( for x0 being Real st x0 in left_open_halfline r holds
diff f,x0 <= 0 ) holds
f is_non_increasing_on left_open_halfline r

for r being Real
for f being PartFunc of REAL , REAL st f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds
0 < diff f,x0 ) holds
( f is_increasing_on right_open_halfline r & f | (right_open_halfline r) is one-to-one )

for r being Real
for f being PartFunc of REAL , REAL st f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds
diff f,x0 < 0 ) holds
( f is_decreasing_on right_open_halfline r & f | (right_open_halfline r) is one-to-one )

for r being Real
for f being PartFunc of REAL , REAL st f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds
0 <= diff f,x0 ) holds
f is_non_decreasing_on right_open_halfline r

for r being Real
for f being PartFunc of REAL , REAL st f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds
diff f,x0 <= 0 ) holds
f is_non_increasing_on right_open_halfline r

for f being PartFunc of REAL , REAL st f is_differentiable_on [#] REAL & ( for x0 being Real holds 0 < diff f,x0 ) holds
( f is_increasing_on [#] REAL & f is one-to-one )

for f being PartFunc of REAL , REAL st f is_differentiable_on [#] REAL & ( for x0 being Real holds diff f,x0 < 0 ) holds
( f is_decreasing_on [#] REAL & f is one-to-one )

for f being PartFunc of REAL , REAL st f is_differentiable_on [#] REAL & ( for x0 being Real holds 0 <= diff f,x0 ) holds
f is_non_decreasing_on [#] REAL

for f being PartFunc of REAL , REAL st f is_differentiable_on [#] REAL & ( for x0 being Real holds diff f,x0 <= 0 ) holds
f is_non_increasing_on [#] REAL

for p, g being Real
for f being PartFunc of REAL , REAL st f is_differentiable_on ].p,g.[ & ( for x0 being Real st x0 in ].p,g.[ holds
0 < diff f,x0 or for x0 being Real st x0 in ].p,g.[ holds
diff f,x0 < 0 ) holds
rng (f | ].p,g.[) is open

for p being Real
for f being PartFunc of REAL , REAL st f is_differentiable_on left_open_halfline p & ( for x0 being Real st x0 in left_open_halfline p holds
0 < diff f,x0 or for x0 being Real st x0 in left_open_halfline p holds
diff f,x0 < 0 ) holds
rng (f | (left_open_halfline p)) is open

for p being Real
for f being PartFunc of REAL , REAL st f is_differentiable_on right_open_halfline p & ( for x0 being Real st x0 in right_open_halfline p holds
0 < diff f,x0 or for x0 being Real st x0 in right_open_halfline p holds
diff f,x0 < 0 ) holds
rng (f | (right_open_halfline p)) is open

for f being PartFunc of REAL , REAL st f is_differentiable_on [#] REAL & ( for x0 being Real holds 0 < diff f,x0 or for x0 being Real holds diff f,x0 < 0 ) holds
rng f is open

for f being one-to-one PartFunc of REAL , REAL st f is_differentiable_on [#] REAL & ( for x0 being Real holds 0 < diff f,x0 or for x0 being Real holds diff f,x0 < 0 ) holds
( f is one-to-one & f " is_differentiable_on dom (f " ) & ( for x0 being Real st x0 in dom (f " ) holds
diff (f " ),x0 = 1 / (diff f,((f " ) . x0)) ) )

for p being Real
for f being one-to-one PartFunc of REAL , REAL st f is_differentiable_on left_open_halfline p & ( for x0 being Real st x0 in left_open_halfline p holds
0 < diff f,x0 or for x0 being Real st x0 in left_open_halfline p holds
diff f,x0 < 0 ) holds
( f | (left_open_halfline p) is one-to-one & (f | (left_open_halfline p)) " is_differentiable_on dom ((f | (left_open_halfline p)) " ) & ( for x0 being Real st x0 in dom ((f | (left_open_halfline p)) " ) holds
diff ((f | (left_open_halfline p)) " ),x0 = 1 / (diff f,(((f | (left_open_halfline p)) " ) . x0)) ) )

for p being Real
for f being one-to-one PartFunc of REAL , REAL st f is_differentiable_on right_open_halfline p & ( for x0 being Real st x0 in right_open_halfline p holds
0 < diff f,x0 or for x0 being Real st x0 in right_open_halfline p holds
diff f,x0 < 0 ) holds
( f | (right_open_halfline p) is one-to-one & (f | (right_open_halfline p)) " is_differentiable_on dom ((f | (right_open_halfline p)) " ) & ( for x0 being Real st x0 in dom ((f | (right_open_halfline p)) " ) holds
diff ((f | (right_open_halfline p)) " ),x0 = 1 / (diff f,(((f | (right_open_halfline p)) " ) . x0)) ) )

for p, g being Real
for f being one-to-one PartFunc of REAL , REAL st f is_differentiable_on ].p,g.[ & ( for x0 being Real st x0 in ].p,g.[ holds
0 < diff f,x0 or for x0 being Real st x0 in ].p,g.[ holds
diff f,x0 < 0 ) holds
( f | ].p,g.[ is one-to-one & (f | ].p,g.[) " is_differentiable_on dom ((f | ].p,g.[) " ) & ( for x0 being Real st x0 in dom ((f | ].p,g.[) " ) holds
diff ((f | ].p,g.[) " ),x0 = 1 / (diff f,(((f | ].p,g.[) " ) . x0)) ) )

for x0 being Real
for f being PartFunc of REAL , REAL st f is_differentiable_in x0 holds
for h being convergent_to_0 Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & rng ((- h) + c) c= dom f holds
( ((2 (#) h) " ) (#) ((f * (c + h)) - (f * (c - h))) is convergent & lim (((2 (#) h) " ) (#) ((f * (c + h)) - (f * (c - h)))) = diff f,x0 )