:: FDIFF_5 semantic presentation

begin

          Lm1:  for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 holds
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = 2 * x ) )
proof
let a be Real; ::_thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 holds
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = 2 * x ) )
let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 holds
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = 2 * x ) )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f1 + f2) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 implies ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = 2 * x ) ) )
assume that
A1: Z c= dom (f1 + f2) and
A2: for x being Real st x in Z holds
f1 . x = a and
A3: f2 = #Z 2 ; ::_thesis: ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = 2 * x ) )
A4: for x being Real st x in Z holds
f2 is_differentiable_in x by A3, TAYLOR_1:2;
A5: Z c= (dom f1) /\ (dom f2) by A1, VALUED_1:def_1;
then A6: Z c= dom f1 by XBOOLE_1:18;
A7: for x being Real st x in Z holds
f1 . x = (0 * x) + a by A2;
then A8: f1 is_differentiable_on Z by A6, FDIFF_1:23;
 Z c= dom f2 by A5, XBOOLE_1:18;
then A9: f2 is_differentiable_on Z by A4, FDIFF_1:9;
A10: for x being Real st x in Z holds
(f2 `| Z) . x = 2 * (x #Z (2 - 1))
proof
let x be Real; ::_thesis: ( x in Z implies (f2 `| Z) . x = 2 * (x #Z (2 - 1)) )
assume A11: x in Z ; ::_thesis: (f2 `| Z) . x = 2 * (x #Z (2 - 1))
 diff (f2,x) = 2 * (x #Z (2 - 1)) by A3, TAYLOR_1:2;
hence  (f2 `| Z) . x = 2 * (x #Z (2 - 1)) by A9, A11, FDIFF_1:def_7; ::_thesis: verum
end;
 for x being Real st x in Z holds
((f1 + f2) `| Z) . x = 2 * x
proof
let x be Real; ::_thesis: ( x in Z implies ((f1 + f2) `| Z) . x = 2 * x )
assume A12: x in Z ; ::_thesis: ((f1 + f2) `| Z) . x = 2 * x
then  ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) by A1, A8, A9, FDIFF_1:18;
hence ((f1 + f2) `| Z) . x = ((f1 `| Z) . x) + (diff (f2,x)) by A8, A12, FDIFF_1:def_7
.= ((f1 `| Z) . x) + ((f2 `| Z) . x) by A9, A12, FDIFF_1:def_7
.= 0 + ((f2 `| Z) . x) by A6, A7, A12, FDIFF_1:23
.= 2 * (x #Z (2 - 1)) by A10, A12
.= 2 * (x |^ 1) by PREPOWER:36
.= 2 * x by NEWTON:5 ;
::_thesis: verum
end;
hence  ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = 2 * x ) ) by A1, A8, A9, FDIFF_1:18; ::_thesis: verum
end;

Lm2:  for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 - f2) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 holds
( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = - (2 * x) ) )
proof
let a be Real; ::_thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 - f2) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 holds
( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = - (2 * x) ) )
let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 - f2) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 holds
( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = - (2 * x) ) )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f1 - f2) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 implies ( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = - (2 * x) ) ) )
assume that
A1: Z c= dom (f1 - f2) and
A2: for x being Real st x in Z holds
f1 . x = a and
A3: f2 = #Z 2 ; ::_thesis: ( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = - (2 * x) ) )
A4: for x being Real st x in Z holds
f2 is_differentiable_in x by A3, TAYLOR_1:2;
A5: Z c= (dom f1) /\ (dom f2) by A1, VALUED_1:12;
then A6: Z c= dom f1 by XBOOLE_1:18;
A7: for x being Real st x in Z holds
f1 . x = (0 * x) + a by A2;
then A8: f1 is_differentiable_on Z by A6, FDIFF_1:23;
 Z c= dom f2 by A5, XBOOLE_1:18;
then A9: f2 is_differentiable_on Z by A4, FDIFF_1:9;
A10: for x being Real st x in Z holds
(f2 `| Z) . x = 2 * (x #Z (2 - 1))
proof
let x be Real; ::_thesis: ( x in Z implies (f2 `| Z) . x = 2 * (x #Z (2 - 1)) )
assume A11: x in Z ; ::_thesis: (f2 `| Z) . x = 2 * (x #Z (2 - 1))
 diff (f2,x) = 2 * (x #Z (2 - 1)) by A3, TAYLOR_1:2;
hence  (f2 `| Z) . x = 2 * (x #Z (2 - 1)) by A9, A11, FDIFF_1:def_7; ::_thesis: verum
end;
 for x being Real st x in Z holds
((f1 - f2) `| Z) . x = - (2 * x)
proof
let x be Real; ::_thesis: ( x in Z implies ((f1 - f2) `| Z) . x = - (2 * x) )
assume A12: x in Z ; ::_thesis: ((f1 - f2) `| Z) . x = - (2 * x)
then  ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) by A1, A8, A9, FDIFF_1:19;
hence ((f1 - f2) `| Z) . x = ((f1 `| Z) . x) - (diff (f2,x)) by A8, A12, FDIFF_1:def_7
.= ((f1 `| Z) . x) - ((f2 `| Z) . x) by A9, A12, FDIFF_1:def_7
.= 0 - ((f2 `| Z) . x) by A6, A7, A12, FDIFF_1:23
.= 0 - (2 * (x #Z (2 - 1))) by A10, A12
.= 0 - (2 * (x |^ 1)) by PREPOWER:36
.= - (2 * (x |^ 1))
.= - (2 * x) by NEWTON:5 ;
::_thesis: verum
end;
hence  ( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = - (2 * x) ) ) by A1, A8, A9, FDIFF_1:19; ::_thesis: verum
end;

Lm3:  for Z being open Subset of REAL st Z c= dom (#R (1 / 2)) holds
( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds
((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (#R (1 / 2)) implies ( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds
((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) ) )
assume A1: Z c= dom (#R (1 / 2)) ; ::_thesis: ( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds
((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) )
A2: for x being Real st x in Z holds
#R (1 / 2) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies #R (1 / 2) is_differentiable_in x )
assume  x in Z ; ::_thesis: #R (1 / 2) is_differentiable_in x
then  x in dom (#R (1 / 2)) by A1;
then  x in right_open_halfline 0 by TAYLOR_1:def_4;
then  x > 0 by XXREAL_1:4;
hence  #R (1 / 2) is_differentiable_in x by TAYLOR_1:21; ::_thesis: verum
end;
then A3: #R (1 / 2) is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2)))
proof
let x be Real; ::_thesis: ( x in Z implies ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) )
assume A4: x in Z ; ::_thesis: ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2)))
then  x in dom (#R (1 / 2)) by A1;
then  x in right_open_halfline 0 by TAYLOR_1:def_4;
then  x > 0 by XXREAL_1:4;
then  diff ((#R (1 / 2)),x) = (1 / 2) * (x #R ((1 / 2) - 1)) by TAYLOR_1:21
.= (1 / 2) * (x #R (- (1 / 2))) ;
hence  ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) by A3, A4, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds
((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) ) by A1, A2, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_5:1
for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = a + x & f2 . x = a - x & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) ) )
proof
let a be Real; ::_thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = a + x & f2 . x = a - x & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) ) )
let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = a + x & f2 . x = a - x & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) ) )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = a + x & f2 . x = a - x & f2 . x <> 0 ) ) implies ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) ) ) )
assume that
A1: Z c= dom (f1 / f2) and
A2: for x being Real st x in Z holds
( f1 . x = a + x & f2 . x = a - x & f2 . x <> 0 ) ; ::_thesis: ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) ) )
A3: Z c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A1, RFUNCT_1:def_1;
then A4: Z c= dom f1 by XBOOLE_1:18;
A5: for x being Real st x in Z holds
f1 . x = (1 * x) + a by A2;
then A6: f1 is_differentiable_on Z by A4, FDIFF_1:23;
A7: for x being Real st x in Z holds
f2 . x = ((- 1) * x) + a
proof
let x be Real; ::_thesis: ( x in Z implies f2 . x = ((- 1) * x) + a )
assume  x in Z ; ::_thesis: f2 . x = ((- 1) * x) + a
then  f2 . x = a - x by A2;
hence  f2 . x = ((- 1) * x) + a ; ::_thesis: verum
end;
A8: Z c= dom f2 by A3, XBOOLE_1:1;
then A9: f2 is_differentiable_on Z by A7, FDIFF_1:23;
A10: for x being Real st x in Z holds
f2 . x <> 0 by A2;
then A11: f1 / f2 is_differentiable_on Z by A6, A9, FDIFF_2:21;
 for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) )
assume A12: x in Z ; ::_thesis: ((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2)
then A13: f2 . x <> 0 by A2;
A14: ( f1 . x = a + x & f2 . x = a - x ) by A2, A12;
 ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A6, A9, A12, FDIFF_1:9;
then  diff ((f1 / f2),x) = (((diff (f1,x)) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2) by A13, FDIFF_2:14
.= ((((f1 `| Z) . x) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2) by A6, A12, FDIFF_1:def_7
.= ((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2) by A9, A12, FDIFF_1:def_7
.= ((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2) by A4, A5, A12, FDIFF_1:23
.= ((1 * (f2 . x)) - ((- 1) * (f1 . x))) / ((f2 . x) ^2) by A8, A7, A12, FDIFF_1:23
.= (2 * a) / ((a - x) ^2) by A14 ;
hence  ((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) by A11, A12, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) ) ) by A6, A9, A10, FDIFF_2:21; ::_thesis: verum
end;

theorem :: FDIFF_5:2
for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x - a & f2 . x = x + a & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) ) )
proof
let a be Real; ::_thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x - a & f2 . x = x + a & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) ) )
let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x - a & f2 . x = x + a & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) ) )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x - a & f2 . x = x + a & f2 . x <> 0 ) ) implies ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) ) ) )
assume that
A1: Z c= dom (f1 / f2) and
A2: for x being Real st x in Z holds
( f1 . x = x - a & f2 . x = x + a & f2 . x <> 0 ) ; ::_thesis: ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) ) )
A3: for x being Real st x in Z holds
f2 . x = (1 * x) + a by A2;
A4: Z c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A1, RFUNCT_1:def_1;
then A5: Z c= dom f1 by XBOOLE_1:18;
A6: Z c= dom f2 by A4, XBOOLE_1:1;
then A7: f2 is_differentiable_on Z by A3, FDIFF_1:23;
A8: for x being Real st x in Z holds
f1 . x = (1 * x) + (- a)
proof
let x be Real; ::_thesis: ( x in Z implies f1 . x = (1 * x) + (- a) )
A9: (1 * x) + (- a) = (1 * x) - a ;
assume  x in Z ; ::_thesis: f1 . x = (1 * x) + (- a)
hence  f1 . x = (1 * x) + (- a) by A2, A9; ::_thesis: verum
end;
then A10: f1 is_differentiable_on Z by A5, FDIFF_1:23;
A11: for x being Real st x in Z holds
f2 . x <> 0 by A2;
then A12: f1 / f2 is_differentiable_on Z by A10, A7, FDIFF_2:21;
 for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) )
assume A13: x in Z ; ::_thesis: ((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2)
then A14: f2 . x <> 0 by A2;
A15: ( f1 . x = x - a & f2 . x = x + a ) by A2, A13;
 ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A10, A7, A13, FDIFF_1:9;
then  diff ((f1 / f2),x) = (((diff (f1,x)) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2) by A14, FDIFF_2:14
.= ((((f1 `| Z) . x) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2) by A10, A13, FDIFF_1:def_7
.= ((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2) by A7, A13, FDIFF_1:def_7
.= ((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2) by A5, A8, A13, FDIFF_1:23
.= ((1 * (f2 . x)) - (1 * (f1 . x))) / ((f2 . x) ^2) by A6, A3, A13, FDIFF_1:23
.= (2 * a) / ((x + a) ^2) by A15 ;
hence  ((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) by A12, A13, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) ) ) by A10, A7, A11, FDIFF_2:21; ::_thesis: verum
end;

theorem :: FDIFF_5:3
for a, b being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x - a & f2 . x = x - b & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) ) )
proof
let a, b be Real; ::_thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x - a & f2 . x = x - b & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) ) )
let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x - a & f2 . x = x - b & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) ) )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x - a & f2 . x = x - b & f2 . x <> 0 ) ) implies ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) ) ) )
assume that
A1: Z c= dom (f1 / f2) and
A2: for x being Real st x in Z holds
( f1 . x = x - a & f2 . x = x - b & f2 . x <> 0 ) ; ::_thesis: ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) ) )
A3: for x being Real st x in Z holds
( f1 . x = (1 * x) + (- a) & f2 . x = (1 * x) + (- b) )
proof
let x be Real; ::_thesis: ( x in Z implies ( f1 . x = (1 * x) + (- a) & f2 . x = (1 * x) + (- b) ) )
A4: ( (1 * x) + (- a) = (1 * x) - a & (1 * x) + (- b) = (1 * x) - b ) ;
assume  x in Z ; ::_thesis: ( f1 . x = (1 * x) + (- a) & f2 . x = (1 * x) + (- b) )
hence  ( f1 . x = (1 * x) + (- a) & f2 . x = (1 * x) + (- b) ) by A2, A4; ::_thesis: verum
end;
then A5: for x being Real st x in Z holds
f1 . x = (1 * x) + (- a) ;
A6: Z c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A1, RFUNCT_1:def_1;
then A7: Z c= dom f1 by XBOOLE_1:18;
then A8: f1 is_differentiable_on Z by A5, FDIFF_1:23;
A9: for x being Real st x in Z holds
f2 . x = (1 * x) + (- b) by A3;
A10: Z c= dom f2 by A6, XBOOLE_1:1;
then A11: f2 is_differentiable_on Z by A9, FDIFF_1:23;
A12: for x being Real st x in Z holds
f2 . x <> 0 by A2;
then A13: f1 / f2 is_differentiable_on Z by A8, A11, FDIFF_2:21;
 for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) )
assume A14: x in Z ; ::_thesis: ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2)
then A15: f2 . x <> 0 by A2;
A16: ( f1 . x = x - a & f2 . x = x - b ) by A2, A14;
 ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A8, A11, A14, FDIFF_1:9;
then  diff ((f1 / f2),x) = (((diff (f1,x)) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2) by A15, FDIFF_2:14
.= ((((f1 `| Z) . x) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2) by A8, A14, FDIFF_1:def_7
.= ((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2) by A11, A14, FDIFF_1:def_7
.= ((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2) by A7, A5, A14, FDIFF_1:23
.= ((1 * (f2 . x)) - (1 * (f1 . x))) / ((f2 . x) ^2) by A10, A9, A14, FDIFF_1:23
.= (a - b) / ((x - b) ^2) by A16 ;
hence  ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) by A13, A14, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) ) ) by A8, A11, A12, FDIFF_2:21; ::_thesis: verum
end;

theorem Th4: :: FDIFF_5:4
for Z being open Subset of REAL st not 0 in Z holds
( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( not 0 in Z implies ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) ) )
set f = id Z;
A1: ( Z c= dom (id Z) & ( for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 ) ) by FUNCT_1:17;
then A2: id Z is_differentiable_on Z by FDIFF_1:23;
assume A3: not 0 in Z ; ::_thesis: ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) )
then A4: for x being Real st x in Z holds
(id Z) . x <> 0 by FUNCT_1:18;
then A5: (id Z) ^ is_differentiable_on Z by A2, FDIFF_2:22;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(((id_Z)_^)_`|_Z)_._x_=_-_(1_/_(x_^2))
let x be Real; ::_thesis: ( x in Z implies (((id Z) ^) `| Z) . x = - (1 / (x ^2)) )
assume A6: x in Z ; ::_thesis: (((id Z) ^) `| Z) . x = - (1 / (x ^2))
then A7: ( (id Z) . x <> 0 & id Z is_differentiable_in x ) by A3, A2, FDIFF_1:9, FUNCT_1:18;
(((id Z) ^) `| Z) . x = diff (((id Z) ^),x) by A5, A6, FDIFF_1:def_7
.= - ((diff ((id Z),x)) / (((id Z) . x) ^2)) by A7, FDIFF_2:15
.= - ((((id Z) `| Z) . x) / (((id Z) . x) ^2)) by A2, A6, FDIFF_1:def_7
.= - (1 / (((id Z) . x) ^2)) by A1, A6, FDIFF_1:23
.= - (1 / (x ^2)) by A6, FUNCT_1:18 ;
hence  (((id Z) ^) `| Z) . x = - (1 / (x ^2)) ; ::_thesis: verum
end;
hence  ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) ) by A2, A4, FDIFF_2:22; ::_thesis: verum
end;

Lm4:  for Z being open Subset of REAL st not 0 in Z holds
dom (sin * ((id Z) ^)) = Z
proof
let Z be open Subset of REAL; ::_thesis: ( not 0 in Z implies dom (sin * ((id Z) ^)) = Z )
A1: rng ((id Z) ^) c= REAL by RELAT_1:def_19;
assume A2: not 0 in Z ; ::_thesis: dom (sin * ((id Z) ^)) = Z
 (id Z) " {0} c= {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (id Z) " {0} or x in {} )
assume A3: x in (id Z) " {0} ; ::_thesis: x in {}
then  x in dom (id Z) by FUNCT_1:def_7;
then A4: x in Z by FUNCT_1:17;
 (id Z) . x in {0} by A3, FUNCT_1:def_7;
then  x in {0} by A4, FUNCT_1:18;
hence  x in {} by A2, A4, TARSKI:def_1; ::_thesis: verum
end;
then A5: (id Z) " {0} = {} by XBOOLE_1:3;
dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def_2
.= Z by A5, FUNCT_1:17 ;
hence  dom (sin * ((id Z) ^)) = Z by A1, RELAT_1:27, SIN_COS:24; ::_thesis: verum
end;

theorem Th5: :: FDIFF_5:5
for Z being open Subset of REAL st not 0 in Z holds
( sin * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( not 0 in Z implies ( sin * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) ) ) )
set f = id Z;
assume A1: not 0 in Z ; ::_thesis: ( sin * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) ) )
then A2: Z c= dom (sin * ((id Z) ^)) by Lm4;
then  for y being set st y in Z holds
y in dom ((id Z) ^) by FUNCT_1:11;
then A3: Z c= dom ((id Z) ^) by TARSKI:def_3;
A4: (id Z) ^ is_differentiable_on Z by A1, Th4;
A5: for x being Real st x in Z holds
sin * ((id Z) ^) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sin * ((id Z) ^) is_differentiable_in x )
assume  x in Z ; ::_thesis: sin * ((id Z) ^) is_differentiable_in x
then A6: (id Z) ^ is_differentiable_in x by A4, FDIFF_1:9;
 sin is_differentiable_in ((id Z) ^) . x by SIN_COS:64;
hence  sin * ((id Z) ^) is_differentiable_in x by A6, FDIFF_2:13; ::_thesis: verum
end;
then A7: sin * ((id Z) ^) is_differentiable_on Z by A2, FDIFF_1:9;
 for x being Real st x in Z holds
((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x)))
proof
let x be Real; ::_thesis: ( x in Z implies ((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) )
A8: sin is_differentiable_in ((id Z) ^) . x by SIN_COS:64;
assume A9: x in Z ; ::_thesis: ((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x)))
then  (id Z) ^ is_differentiable_in x by A4, FDIFF_1:9;
then  diff ((sin * ((id Z) ^)),x) = (diff (sin,(((id Z) ^) . x))) * (diff (((id Z) ^),x)) by A8, FDIFF_2:13
.= (cos . (((id Z) ^) . x)) * (diff (((id Z) ^),x)) by SIN_COS:64
.= (cos . (((id Z) . x) ")) * (diff (((id Z) ^),x)) by A3, A9, RFUNCT_1:def_2
.= (cos . (((id Z) . x) ")) * ((((id Z) ^) `| Z) . x) by A4, A9, FDIFF_1:def_7
.= (cos . (((id Z) . x) ")) * (- (1 / (x ^2))) by A1, A9, Th4
.= (cos . (1 * (x "))) * (- (1 / (x ^2))) by A9, FUNCT_1:18
.= (cos . (1 / x)) * (- (1 / (x ^2))) by XCMPLX_0:def_9 ;
hence  ((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) by A7, A9, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sin * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) ) ) by A2, A5, FDIFF_1:9; ::_thesis: verum
end;

theorem Th6: :: FDIFF_5:6
for Z being open Subset of REAL st not 0 in Z & Z c= dom (cos * ((id Z) ^)) holds
( cos * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & Z c= dom (cos * ((id Z) ^)) implies ( cos * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) ) ) )
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (cos * ((id Z) ^)) ; ::_thesis: ( cos * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) ) )
 for y being set st y in Z holds
y in dom ((id Z) ^) by A2, FUNCT_1:11;
then A3: Z c= dom ((id Z) ^) by TARSKI:def_3;
A4: (id Z) ^ is_differentiable_on Z by A1, Th4;
A5: for x being Real st x in Z holds
cos * ((id Z) ^) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cos * ((id Z) ^) is_differentiable_in x )
assume  x in Z ; ::_thesis: cos * ((id Z) ^) is_differentiable_in x
then A6: (id Z) ^ is_differentiable_in x by A4, FDIFF_1:9;
 cos is_differentiable_in ((id Z) ^) . x by SIN_COS:63;
hence  cos * ((id Z) ^) is_differentiable_in x by A6, FDIFF_2:13; ::_thesis: verum
end;
then A7: cos * ((id Z) ^) is_differentiable_on Z by A2, FDIFF_1:9;
 for x being Real st x in Z holds
((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x))
proof
let x be Real; ::_thesis: ( x in Z implies ((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) )
A8: diff (cos,(((id Z) ^) . x)) = - (sin . (((id Z) ^) . x)) by SIN_COS:63;
A9: cos is_differentiable_in ((id Z) ^) . x by SIN_COS:63;
assume A10: x in Z ; ::_thesis: ((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x))
then  (id Z) ^ is_differentiable_in x by A4, FDIFF_1:9;
then  diff ((cos * ((id Z) ^)),x) = (diff (cos,(((id Z) ^) . x))) * (diff (((id Z) ^),x)) by A9, FDIFF_2:13
.= - ((sin . (((id Z) ^) . x)) * (diff (((id Z) ^),x))) by A8
.= - ((sin . (((id Z) . x) ")) * (diff (((id Z) ^),x))) by A3, A10, RFUNCT_1:def_2
.= - ((sin . (((id Z) . x) ")) * ((((id Z) ^) `| Z) . x)) by A4, A10, FDIFF_1:def_7
.= - ((sin . (((id Z) . x) ")) * (- (1 / (x ^2)))) by A1, A10, Th4
.= - ((sin . (1 * (x "))) * (- (1 / (x ^2)))) by A10, FUNCT_1:18
.= - ((sin . (1 / x)) * (- (1 / (x ^2)))) by XCMPLX_0:def_9
.= (sin . (1 / x)) * (1 / (x ^2)) ;
hence  ((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) by A7, A10, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cos * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) ) ) by A2, A5, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_5:7
for Z being open Subset of REAL st Z c= dom ((id Z) (#) (sin * ((id Z) ^))) & not 0 in Z holds
( (id Z) (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((id Z) (#) (sin * ((id Z) ^))) & not 0 in Z implies ( (id Z) (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ) ) )
set f = id Z;
assume that
A1: Z c= dom ((id Z) (#) (sin * ((id Z) ^))) and
A2: not 0 in Z ; ::_thesis: ( (id Z) (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ) )
A3: sin * ((id Z) ^) is_differentiable_on Z by A2, Th5;
A4: Z c= (dom (id Z)) /\ (dom (sin * ((id Z) ^))) by A1, VALUED_1:def_4;
then A5: Z c= dom (id Z) by XBOOLE_1:18;
A6: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:18;
then A7: id Z is_differentiable_on Z by A5, FDIFF_1:23;
A8: Z c= dom (sin * ((id Z) ^)) by A4, XBOOLE_1:18;
then  for y being set st y in Z holds
y in dom ((id Z) ^) by FUNCT_1:11;
then A9: Z c= dom ((id Z) ^) by TARSKI:def_3;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(((id_Z)_(#)_(sin_*_((id_Z)_^)))_`|_Z)_._x_=_(sin_._(1_/_x))_-_((1_/_x)_*_(cos_._(1_/_x)))
let x be Real; ::_thesis: ( x in Z implies (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) )
assume A10: x in Z ; ::_thesis: (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x)))
then (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (((sin * ((id Z) ^)) . x) * (diff ((id Z),x))) + (((id Z) . x) * (diff ((sin * ((id Z) ^)),x))) by A1, A3, A7, FDIFF_1:21
.= (((sin * ((id Z) ^)) . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff ((sin * ((id Z) ^)),x))) by A7, A10, FDIFF_1:def_7
.= (((sin * ((id Z) ^)) . x) * 1) + (((id Z) . x) * (diff ((sin * ((id Z) ^)),x))) by A5, A6, A10, FDIFF_1:23
.= ((sin * ((id Z) ^)) . x) + (x * (diff ((sin * ((id Z) ^)),x))) by A10, FUNCT_1:18
.= ((sin * ((id Z) ^)) . x) + (x * (((sin * ((id Z) ^)) `| Z) . x)) by A3, A10, FDIFF_1:def_7
.= ((sin * ((id Z) ^)) . x) + (x * (- ((1 / (x ^2)) * (cos . (1 / x))))) by A2, A10, Th5
.= ((sin * ((id Z) ^)) . x) - ((x * (1 / (x * x))) * (cos . (1 / x)))
.= ((sin * ((id Z) ^)) . x) - ((x * ((1 / x) * (1 / x))) * (cos . (1 / x))) by XCMPLX_1:102
.= ((sin * ((id Z) ^)) . x) - (((x * (1 / x)) * (1 / x)) * (cos . (1 / x)))
.= ((sin * ((id Z) ^)) . x) - ((1 * (1 / x)) * (cos . (1 / x))) by A2, A10, XCMPLX_1:106
.= (sin . (((id Z) ^) . x)) - ((1 / x) * (cos . (1 / x))) by A8, A10, FUNCT_1:12
.= (sin . (((id Z) . x) ")) - ((1 / x) * (cos . (1 / x))) by A9, A10, RFUNCT_1:def_2
.= (sin . (1 * (x "))) - ((1 / x) * (cos . (1 / x))) by A10, FUNCT_1:18
.= (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) by XCMPLX_0:def_9 ;
hence  (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ; ::_thesis: verum
end;
hence  ( (id Z) (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ) ) by A1, A3, A7, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_5:8
for Z being open Subset of REAL st Z c= dom ((id Z) (#) (cos * ((id Z) ^))) & not 0 in Z holds
( (id Z) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((id Z) (#) (cos * ((id Z) ^))) & not 0 in Z implies ( (id Z) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) ) )
set f = id Z;
assume that
A1: Z c= dom ((id Z) (#) (cos * ((id Z) ^))) and
A2: not 0 in Z ; ::_thesis: ( (id Z) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) )
A3: Z c= (dom (id Z)) /\ (dom (cos * ((id Z) ^))) by A1, VALUED_1:def_4;
then A4: Z c= dom (cos * ((id Z) ^)) by XBOOLE_1:18;
then A5: cos * ((id Z) ^) is_differentiable_on Z by A2, Th6;
A6: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:18;
A7: Z c= dom (id Z) by A3, XBOOLE_1:18;
then A8: id Z is_differentiable_on Z by A6, FDIFF_1:23;
 for y being set st y in Z holds
y in dom ((id Z) ^) by A4, FUNCT_1:11;
then A9: Z c= dom ((id Z) ^) by TARSKI:def_3;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(((id_Z)_(#)_(cos_*_((id_Z)_^)))_`|_Z)_._x_=_(cos_._(1_/_x))_+_((1_/_x)_*_(sin_._(1_/_x)))
let x be Real; ::_thesis: ( x in Z implies (((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) )
assume A10: x in Z ; ::_thesis: (((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x)))
then (((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (((cos * ((id Z) ^)) . x) * (diff ((id Z),x))) + (((id Z) . x) * (diff ((cos * ((id Z) ^)),x))) by A1, A5, A8, FDIFF_1:21
.= (((cos * ((id Z) ^)) . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff ((cos * ((id Z) ^)),x))) by A8, A10, FDIFF_1:def_7
.= (((cos * ((id Z) ^)) . x) * 1) + (((id Z) . x) * (diff ((cos * ((id Z) ^)),x))) by A7, A6, A10, FDIFF_1:23
.= ((cos * ((id Z) ^)) . x) + (x * (diff ((cos * ((id Z) ^)),x))) by A10, FUNCT_1:18
.= ((cos * ((id Z) ^)) . x) + (x * (((cos * ((id Z) ^)) `| Z) . x)) by A5, A10, FDIFF_1:def_7
.= ((cos * ((id Z) ^)) . x) + (x * ((1 / (x ^2)) * (sin . (1 / x)))) by A2, A4, A10, Th6
.= ((cos * ((id Z) ^)) . x) + ((x * (1 / (x * x))) * (sin . (1 / x)))
.= ((cos * ((id Z) ^)) . x) + ((x * ((1 / x) * (1 / x))) * (sin . (1 / x))) by XCMPLX_1:102
.= ((cos * ((id Z) ^)) . x) + (((x * (1 / x)) * (1 / x)) * (sin . (1 / x)))
.= ((cos * ((id Z) ^)) . x) + ((1 * (1 / x)) * (sin . (1 / x))) by A2, A10, XCMPLX_1:106
.= (cos . (((id Z) ^) . x)) + ((1 / x) * (sin . (1 / x))) by A4, A10, FUNCT_1:12
.= (cos . (((id Z) . x) ")) + ((1 / x) * (sin . (1 / x))) by A9, A10, RFUNCT_1:def_2
.= (cos . (1 * (x "))) + ((1 / x) * (sin . (1 / x))) by A10, FUNCT_1:18
.= (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) by XCMPLX_0:def_9 ;
hence  (((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ; ::_thesis: verum
end;
hence  ( (id Z) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) ) by A1, A5, A8, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_5:9
for Z being open Subset of REAL st Z c= dom ((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) & not 0 in Z holds
( (sin * ((id Z) ^)) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) & not 0 in Z implies ( (sin * ((id Z) ^)) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ) ) )
set f = id Z;
assume that
A1: Z c= dom ((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) and
A2: not 0 in Z ; ::_thesis: ( (sin * ((id Z) ^)) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ) )
A3: sin * ((id Z) ^) is_differentiable_on Z by A2, Th5;
A4: Z c= (dom (sin * ((id Z) ^))) /\ (dom (cos * ((id Z) ^))) by A1, VALUED_1:def_4;
then A5: Z c= dom (cos * ((id Z) ^)) by XBOOLE_1:18;
then A6: cos * ((id Z) ^) is_differentiable_on Z by A2, Th6;
A7: Z c= dom (sin * ((id Z) ^)) by A4, XBOOLE_1:18;
then  for y being set st y in Z holds
y in dom ((id Z) ^) by FUNCT_1:11;
then A8: Z c= dom ((id Z) ^) by TARSKI:def_3;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(((sin_*_((id_Z)_^))_(#)_(cos_*_((id_Z)_^)))_`|_Z)_._x_=_(1_/_(x_^2))_*_(((sin_._(1_/_x))_^2)_-_((cos_._(1_/_x))_^2))
let x be Real; ::_thesis: ( x in Z implies (((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) )
assume A9: x in Z ; ::_thesis: (((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2))
then (((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (((cos * ((id Z) ^)) . x) * (diff ((sin * ((id Z) ^)),x))) + (((sin * ((id Z) ^)) . x) * (diff ((cos * ((id Z) ^)),x))) by A1, A6, A3, FDIFF_1:21
.= (((cos * ((id Z) ^)) . x) * (((sin * ((id Z) ^)) `| Z) . x)) + (((sin * ((id Z) ^)) . x) * (diff ((cos * ((id Z) ^)),x))) by A3, A9, FDIFF_1:def_7
.= (((cos * ((id Z) ^)) . x) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * (diff ((cos * ((id Z) ^)),x))) by A2, A9, Th5
.= (((cos * ((id Z) ^)) . x) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * (((cos * ((id Z) ^)) `| Z) . x)) by A6, A9, FDIFF_1:def_7
.= (((cos * ((id Z) ^)) . x) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / x)))) by A2, A5, A9, Th6
.= ((cos . (((id Z) ^) . x)) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / x)))) by A5, A9, FUNCT_1:12
.= ((cos . (((id Z) . x) ")) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / x)))) by A8, A9, RFUNCT_1:def_2
.= ((cos . (1 * (x "))) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / x)))) by A9, FUNCT_1:18
.= ((cos . (1 / x)) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / x)))) by XCMPLX_0:def_9
.= ((cos . (1 / x)) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + ((sin . (((id Z) ^) . x)) * ((1 / (x ^2)) * (sin . (1 / x)))) by A7, A9, FUNCT_1:12
.= ((cos . (1 / x)) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + ((sin . (((id Z) . x) ")) * ((1 / (x ^2)) * (sin . (1 / x)))) by A8, A9, RFUNCT_1:def_2
.= ((cos . (1 / x)) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + ((sin . (1 * (x "))) * ((1 / (x ^2)) * (sin . (1 / x)))) by A9, FUNCT_1:18
.= (- (((cos . (1 / x)) * (1 / (x ^2))) * (cos . (1 / x)))) + ((sin . (1 / x)) * ((1 / (x ^2)) * (sin . (1 / x)))) by XCMPLX_0:def_9
.= (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ;
hence  (((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ; ::_thesis: verum
end;
hence  ( (sin * ((id Z) ^)) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ) ) by A1, A6, A3, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_5:10
for n being Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (sin * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) )
proof
let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (sin * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) )
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (sin * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((sin * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) implies ( (sin * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) ) )
assume that
A1: Z c= dom ((sin * f) (#) ((#Z n) * sin)) and
A2: n >= 1 and
A3: for x being Real st x in Z holds
f . x = n * x ; ::_thesis: ( (sin * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) )
A4: for x being Real st x in Z holds
f . x = (n * x) + 0 by A3;
A5: Z c= (dom (sin * f)) /\ (dom ((#Z n) * sin)) by A1, VALUED_1:def_4;
then A6: Z c= dom (sin * f) by XBOOLE_1:18;
then  for y being set st y in Z holds
y in dom f by FUNCT_1:11;
then A7: Z c= dom f by TARSKI:def_3;
then A8: f is_differentiable_on Z by A4, FDIFF_1:23;
 for x being Real st x in Z holds
sin * f is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sin * f is_differentiable_in x )
assume  x in Z ; ::_thesis: sin * f is_differentiable_in x
then A9: f is_differentiable_in x by A8, FDIFF_1:9;
 sin is_differentiable_in f . x by SIN_COS:64;
hence  sin * f is_differentiable_in x by A9, FDIFF_2:13; ::_thesis: verum
end;
then A10: sin * f is_differentiable_on Z by A6, FDIFF_1:9;
A11: for x being Real st x in Z holds
((sin * f) `| Z) . x = n * (cos . (n * x))
proof
let x be Real; ::_thesis: ( x in Z implies ((sin * f) `| Z) . x = n * (cos . (n * x)) )
A12: sin is_differentiable_in f . x by SIN_COS:64;
assume A13: x in Z ; ::_thesis: ((sin * f) `| Z) . x = n * (cos . (n * x))
then  f is_differentiable_in x by A8, FDIFF_1:9;
then  diff ((sin * f),x) = (diff (sin,(f . x))) * (diff (f,x)) by A12, FDIFF_2:13
.= (cos . (f . x)) * (diff (f,x)) by SIN_COS:64
.= (cos . (n * x)) * (diff (f,x)) by A3, A13
.= (cos . (n * x)) * ((f `| Z) . x) by A8, A13, FDIFF_1:def_7
.= n * (cos . (n * x)) by A7, A4, A13, FDIFF_1:23 ;
hence  ((sin * f) `| Z) . x = n * (cos . (n * x)) by A10, A13, FDIFF_1:def_7; ::_thesis: verum
end;
A14: Z c= dom ((#Z n) * sin) by A5, XBOOLE_1:18;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(#Z_n)_*_sin_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies (#Z n) * sin is_differentiable_in x )
assume  x in Z ; ::_thesis: (#Z n) * sin is_differentiable_in x
 sin is_differentiable_in x by SIN_COS:64;
hence  (#Z n) * sin is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum
end;
then A15: (#Z n) * sin is_differentiable_on Z by A14, FDIFF_1:9;
A16: for x being Real st x in Z holds
(((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x)
proof
let x be Real; ::_thesis: ( x in Z implies (((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x) )
 sin is_differentiable_in x by SIN_COS:64;
then A17: diff (((#Z n) * sin),x) = (n * ((sin . x) #Z (n - 1))) * (diff (sin,x)) by TAYLOR_1:3
.= (n * ((sin . x) #Z (n - 1))) * (cos . x) by SIN_COS:64 ;
assume  x in Z ; ::_thesis: (((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x)
hence  (((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x) by A15, A17, FDIFF_1:def_7; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(((sin_*_f)_(#)_((#Z_n)_*_sin))_`|_Z)_._x_=_(n_*_((sin_._x)_#Z_(n_-_1)))_*_(sin_._((n_+_1)_*_x))
let x be Real; ::_thesis: ( x in Z implies (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) )
A18: n - 1 is Element of NAT by A2, NAT_1:21;
assume A19: x in Z ; ::_thesis: (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x))
then (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = ((((#Z n) * sin) . x) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * sin),x))) by A1, A10, A15, FDIFF_1:21
.= (((#Z n) . (sin . x)) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * sin),x))) by A14, A19, FUNCT_1:12
.= (((sin . x) #Z n) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * sin),x))) by TAYLOR_1:def_1
.= (((sin . x) #Z n) * (((sin * f) `| Z) . x)) + (((sin * f) . x) * (diff (((#Z n) * sin),x))) by A10, A19, FDIFF_1:def_7
.= (((sin . x) #Z n) * (n * (cos . (n * x)))) + (((sin * f) . x) * (diff (((#Z n) * sin),x))) by A11, A19
.= (((sin . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (f . x)) * (diff (((#Z n) * sin),x))) by A6, A19, FUNCT_1:12
.= (((sin . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * (diff (((#Z n) * sin),x))) by A3, A19
.= (((sin . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * ((((#Z n) * sin) `| Z) . x)) by A15, A19, FDIFF_1:def_7
.= (((sin . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * ((n * ((sin . x) #Z (n - 1))) * (cos . x))) by A16, A19
.= (((sin . x) #Z ((n - 1) + 1)) * (n * (cos . (n * x)))) + ((((sin . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x))
.= ((((sin . x) #Z (n - 1)) * ((sin . x) #Z 1)) * (n * (cos . (n * x)))) + ((((sin . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x)) by A18, TAYLOR_1:1
.= ((((sin . x) #Z (n - 1)) * (sin . x)) * (n * (cos . (n * x)))) + ((((sin . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x)) by PREPOWER:35
.= (n * ((sin . x) #Z (n - 1))) * (((sin . x) * (cos . (n * x))) + ((cos . x) * (sin . (n * x))))
.= (n * ((sin . x) #Z (n - 1))) * (sin . (x + (n * x))) by SIN_COS:74
.= (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ;
hence  (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ; ::_thesis: verum
end;
hence  ( (sin * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) ) by A1, A10, A15, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_5:11
for n being Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (cos * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )
proof
let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (cos * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (cos * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((cos * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) implies ( (cos * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) )
assume that
A1: Z c= dom ((cos * f) (#) ((#Z n) * sin)) and
A2: n >= 1 and
A3: for x being Real st x in Z holds
f . x = n * x ; ::_thesis: ( (cos * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )
A4: for x being Real st x in Z holds
f . x = (n * x) + 0 by A3;
A5: Z c= (dom (cos * f)) /\ (dom ((#Z n) * sin)) by A1, VALUED_1:def_4;
then A6: Z c= dom (cos * f) by XBOOLE_1:18;
then  for y being set st y in Z holds
y in dom f by FUNCT_1:11;
then A7: Z c= dom f by TARSKI:def_3;
then A8: f is_differentiable_on Z by A4, FDIFF_1:23;
 for x being Real st x in Z holds
cos * f is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cos * f is_differentiable_in x )
assume  x in Z ; ::_thesis: cos * f is_differentiable_in x
then A9: f is_differentiable_in x by A8, FDIFF_1:9;
 cos is_differentiable_in f . x by SIN_COS:63;
hence  cos * f is_differentiable_in x by A9, FDIFF_2:13; ::_thesis: verum
end;
then A10: cos * f is_differentiable_on Z by A6, FDIFF_1:9;
A11: for x being Real st x in Z holds
((cos * f) `| Z) . x = - (n * (sin . (n * x)))
proof
let x be Real; ::_thesis: ( x in Z implies ((cos * f) `| Z) . x = - (n * (sin . (n * x))) )
A12: cos is_differentiable_in f . x by SIN_COS:63;
assume A13: x in Z ; ::_thesis: ((cos * f) `| Z) . x = - (n * (sin . (n * x)))
then  f is_differentiable_in x by A8, FDIFF_1:9;
then  diff ((cos * f),x) = (diff (cos,(f . x))) * (diff (f,x)) by A12, FDIFF_2:13
.= (- (sin . (f . x))) * (diff (f,x)) by SIN_COS:63
.= (- (sin . (n * x))) * (diff (f,x)) by A3, A13
.= (- (sin . (n * x))) * ((f `| Z) . x) by A8, A13, FDIFF_1:def_7
.= (- (sin . (n * x))) * n by A7, A4, A13, FDIFF_1:23
.= - (n * (sin . (n * x))) ;
hence  ((cos * f) `| Z) . x = - (n * (sin . (n * x))) by A10, A13, FDIFF_1:def_7; ::_thesis: verum
end;
A14: Z c= dom ((#Z n) * sin) by A5, XBOOLE_1:18;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(#Z_n)_*_sin_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies (#Z n) * sin is_differentiable_in x )
assume  x in Z ; ::_thesis: (#Z n) * sin is_differentiable_in x
 sin is_differentiable_in x by SIN_COS:64;
hence  (#Z n) * sin is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum
end;
then A15: (#Z n) * sin is_differentiable_on Z by A14, FDIFF_1:9;
A16: for x being Real st x in Z holds
(((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x)
proof
let x be Real; ::_thesis: ( x in Z implies (((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x) )
 sin is_differentiable_in x by SIN_COS:64;
then A17: diff (((#Z n) * sin),x) = (n * ((sin . x) #Z (n - 1))) * (diff (sin,x)) by TAYLOR_1:3
.= (n * ((sin . x) #Z (n - 1))) * (cos . x) by SIN_COS:64 ;
assume  x in Z ; ::_thesis: (((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x)
hence  (((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x) by A15, A17, FDIFF_1:def_7; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(((cos_*_f)_(#)_((#Z_n)_*_sin))_`|_Z)_._x_=_(n_*_((sin_._x)_#Z_(n_-_1)))_*_(cos_._((n_+_1)_*_x))
let x be Real; ::_thesis: ( x in Z implies (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) )
A18: n - 1 is Element of NAT by A2, NAT_1:21;
assume A19: x in Z ; ::_thesis: (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x))
then (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = ((((#Z n) * sin) . x) * (diff ((cos * f),x))) + (((cos * f) . x) * (diff (((#Z n) * sin),x))) by A1, A10, A15, FDIFF_1:21
.= (((#Z n) . (sin . x)) * (diff ((cos * f),x))) + (((cos * f) . x) * (diff (((#Z n) * sin),x))) by A14, A19, FUNCT_1:12
.= (((sin . x) #Z n) * (diff ((cos * f),x))) + (((cos * f) . x) * (diff (((#Z n) * sin),x))) by TAYLOR_1:def_1
.= (((sin . x) #Z n) * (((cos * f) `| Z) . x)) + (((cos * f) . x) * (diff (((#Z n) * sin),x))) by A10, A19, FDIFF_1:def_7
.= (((sin . x) #Z n) * (- (n * (sin . (n * x))))) + (((cos * f) . x) * (diff (((#Z n) * sin),x))) by A11, A19
.= (((sin . x) #Z n) * (- (n * (sin . (n * x))))) + ((cos . (f . x)) * (diff (((#Z n) * sin),x))) by A6, A19, FUNCT_1:12
.= (((sin . x) #Z n) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * (diff (((#Z n) * sin),x))) by A3, A19
.= (((sin . x) #Z n) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * ((((#Z n) * sin) `| Z) . x)) by A15, A19, FDIFF_1:def_7
.= (((sin . x) #Z n) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * ((n * ((sin . x) #Z (n - 1))) * (cos . x))) by A16, A19
.= (((sin . x) #Z ((n - 1) + 1)) * (- (n * (sin . (n * x))))) + ((((cos . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x))
.= ((((sin . x) #Z (n - 1)) * ((sin . x) #Z 1)) * (- (n * (sin . (n * x))))) + ((((cos . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x)) by A18, TAYLOR_1:1
.= ((((sin . x) #Z (n - 1)) * (sin . x)) * (- (n * (sin . (n * x))))) + ((((cos . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x)) by PREPOWER:35
.= (n * ((sin . x) #Z (n - 1))) * (((cos . (n * x)) * (cos . x)) - ((sin . x) * (sin . (n * x))))
.= (n * ((sin . x) #Z (n - 1))) * (cos . (x + (n * x))) by SIN_COS:74
.= (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ;
hence  (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ; ::_thesis: verum
end;
hence  ( (cos * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) by A1, A10, A15, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_5:12
for n being Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (cos * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) )
proof
let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (cos * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) )
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (cos * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((cos * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) implies ( (cos * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) ) )
assume that
A1: Z c= dom ((cos * f) (#) ((#Z n) * cos)) and
A2: n >= 1 and
A3: for x being Real st x in Z holds
f . x = n * x ; ::_thesis: ( (cos * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) )
A4: for x being Real st x in Z holds
f . x = (n * x) + 0 by A3;
A5: Z c= (dom (cos * f)) /\ (dom ((#Z n) * cos)) by A1, VALUED_1:def_4;
then A6: Z c= dom (cos * f) by XBOOLE_1:18;
then  for y being set st y in Z holds
y in dom f by FUNCT_1:11;
then A7: Z c= dom f by TARSKI:def_3;
then A8: f is_differentiable_on Z by A4, FDIFF_1:23;
 for x being Real st x in Z holds
cos * f is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cos * f is_differentiable_in x )
assume  x in Z ; ::_thesis: cos * f is_differentiable_in x
then A9: f is_differentiable_in x by A8, FDIFF_1:9;
 cos is_differentiable_in f . x by SIN_COS:63;
hence  cos * f is_differentiable_in x by A9, FDIFF_2:13; ::_thesis: verum
end;
then A10: cos * f is_differentiable_on Z by A6, FDIFF_1:9;
A11: for x being Real st x in Z holds
((cos * f) `| Z) . x = - (n * (sin . (n * x)))
proof
let x be Real; ::_thesis: ( x in Z implies ((cos * f) `| Z) . x = - (n * (sin . (n * x))) )
A12: cos is_differentiable_in f . x by SIN_COS:63;
assume A13: x in Z ; ::_thesis: ((cos * f) `| Z) . x = - (n * (sin . (n * x)))
then  f is_differentiable_in x by A8, FDIFF_1:9;
then  diff ((cos * f),x) = (diff (cos,(f . x))) * (diff (f,x)) by A12, FDIFF_2:13
.= (- (sin . (f . x))) * (diff (f,x)) by SIN_COS:63
.= - ((sin . (f . x)) * (diff (f,x)))
.= - ((sin . (n * x)) * (diff (f,x))) by A3, A13
.= - ((sin . (n * x)) * ((f `| Z) . x)) by A8, A13, FDIFF_1:def_7
.= - (n * (sin . (n * x))) by A7, A4, A13, FDIFF_1:23 ;
hence  ((cos * f) `| Z) . x = - (n * (sin . (n * x))) by A10, A13, FDIFF_1:def_7; ::_thesis: verum
end;
A14: Z c= dom ((#Z n) * cos) by A5, XBOOLE_1:18;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(#Z_n)_*_cos_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies (#Z n) * cos is_differentiable_in x )
assume  x in Z ; ::_thesis: (#Z n) * cos is_differentiable_in x
 cos is_differentiable_in x by SIN_COS:63;
hence  (#Z n) * cos is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum
end;
then A15: (#Z n) * cos is_differentiable_on Z by A14, FDIFF_1:9;
A16: for x being Real st x in Z holds
(((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x))
proof
let x be Real; ::_thesis: ( x in Z implies (((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) )
 cos is_differentiable_in x by SIN_COS:63;
then A17: diff (((#Z n) * cos),x) = (n * ((cos . x) #Z (n - 1))) * (diff (cos,x)) by TAYLOR_1:3
.= (n * ((cos . x) #Z (n - 1))) * (- (sin . x)) by SIN_COS:63
.= - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) ;
assume  x in Z ; ::_thesis: (((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x))
hence  (((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) by A15, A17, FDIFF_1:def_7; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(((cos_*_f)_(#)_((#Z_n)_*_cos))_`|_Z)_._x_=_-_((n_*_((cos_._x)_#Z_(n_-_1)))_*_(sin_._((n_+_1)_*_x)))
let x be Real; ::_thesis: ( x in Z implies (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) )
A18: n - 1 is Element of NAT by A2, NAT_1:21;
assume A19: x in Z ; ::_thesis: (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x)))
then (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = ((((#Z n) * cos) . x) * (diff ((cos * f),x))) + (((cos * f) . x) * (diff (((#Z n) * cos),x))) by A1, A10, A15, FDIFF_1:21
.= (((#Z n) . (cos . x)) * (diff ((cos * f),x))) + (((cos * f) . x) * (diff (((#Z n) * cos),x))) by A14, A19, FUNCT_1:12
.= (((cos . x) #Z n) * (diff ((cos * f),x))) + (((cos * f) . x) * (diff (((#Z n) * cos),x))) by TAYLOR_1:def_1
.= (((cos . x) #Z n) * (((cos * f) `| Z) . x)) + (((cos * f) . x) * (diff (((#Z n) * cos),x))) by A10, A19, FDIFF_1:def_7
.= (((cos . x) #Z n) * (- (n * (sin . (n * x))))) + (((cos * f) . x) * (diff (((#Z n) * cos),x))) by A11, A19
.= (((cos . x) #Z n) * (- (n * (sin . (n * x))))) + ((cos . (f . x)) * (diff (((#Z n) * cos),x))) by A6, A19, FUNCT_1:12
.= (((cos . x) #Z n) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * (diff (((#Z n) * cos),x))) by A3, A19
.= (((cos . x) #Z n) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * ((((#Z n) * cos) `| Z) . x)) by A15, A19, FDIFF_1:def_7
.= (((cos . x) #Z ((n - 1) + 1)) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * (- ((n * ((cos . x) #Z (n - 1))) * (sin . x)))) by A16, A19
.= ((((cos . x) #Z (n - 1)) * ((cos . x) #Z 1)) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * (- ((n * ((cos . x) #Z (n - 1))) * (sin . x)))) by A18, TAYLOR_1:1
.= ((((cos . x) #Z (n - 1)) * (cos . x)) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * (- ((n * ((cos . x) #Z (n - 1))) * (sin . x)))) by PREPOWER:35
.= - ((n * ((cos . x) #Z (n - 1))) * (((sin . (n * x)) * (cos . x)) + ((cos . (n * x)) * (sin . x))))
.= - ((n * ((cos . x) #Z (n - 1))) * (sin . (x + (n * x)))) by SIN_COS:74
.= - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ;
hence  (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ; ::_thesis: verum
end;
hence  ( (cos * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) ) by A1, A10, A15, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_5:13
for n being Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )
proof
let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((sin * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) implies ( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) )
assume that
A1: Z c= dom ((sin * f) (#) ((#Z n) * cos)) and
A2: n >= 1 and
A3: for x being Real st x in Z holds
f . x = n * x ; ::_thesis: ( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )
A4: for x being Real st x in Z holds
f . x = (n * x) + 0 by A3;
A5: Z c= (dom (sin * f)) /\ (dom ((#Z n) * cos)) by A1, VALUED_1:def_4;
then A6: Z c= dom (sin * f) by XBOOLE_1:18;
then  for y being set st y in Z holds
y in dom f by FUNCT_1:11;
then A7: Z c= dom f by TARSKI:def_3;
then A8: f is_differentiable_on Z by A4, FDIFF_1:23;
 for x being Real st x in Z holds
sin * f is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sin * f is_differentiable_in x )
assume  x in Z ; ::_thesis: sin * f is_differentiable_in x
then A9: f is_differentiable_in x by A8, FDIFF_1:9;
 sin is_differentiable_in f . x by SIN_COS:64;
hence  sin * f is_differentiable_in x by A9, FDIFF_2:13; ::_thesis: verum
end;
then A10: sin * f is_differentiable_on Z by A6, FDIFF_1:9;
A11: for x being Real st x in Z holds
((sin * f) `| Z) . x = n * (cos . (n * x))
proof
let x be Real; ::_thesis: ( x in Z implies ((sin * f) `| Z) . x = n * (cos . (n * x)) )
A12: sin is_differentiable_in f . x by SIN_COS:64;
assume A13: x in Z ; ::_thesis: ((sin * f) `| Z) . x = n * (cos . (n * x))
then  f is_differentiable_in x by A8, FDIFF_1:9;
then  diff ((sin * f),x) = (diff (sin,(f . x))) * (diff (f,x)) by A12, FDIFF_2:13
.= (cos . (f . x)) * (diff (f,x)) by SIN_COS:64
.= (cos . (n * x)) * (diff (f,x)) by A3, A13
.= (cos . (n * x)) * ((f `| Z) . x) by A8, A13, FDIFF_1:def_7
.= n * (cos . (n * x)) by A7, A4, A13, FDIFF_1:23 ;
hence  ((sin * f) `| Z) . x = n * (cos . (n * x)) by A10, A13, FDIFF_1:def_7; ::_thesis: verum
end;
A14: Z c= dom ((#Z n) * cos) by A5, XBOOLE_1:18;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(#Z_n)_*_cos_is_differentiable_in_x
let x be Real; ::_thesis: ( x in Z implies (#Z n) * cos is_differentiable_in x )
assume  x in Z ; ::_thesis: (#Z n) * cos is_differentiable_in x
 cos is_differentiable_in x by SIN_COS:63;
hence  (#Z n) * cos is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum
end;
then A15: (#Z n) * cos is_differentiable_on Z by A14, FDIFF_1:9;
A16: for x being Real st x in Z holds
(((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x))
proof
let x be Real; ::_thesis: ( x in Z implies (((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) )
 cos is_differentiable_in x by SIN_COS:63;
then A17: diff (((#Z n) * cos),x) = (n * ((cos . x) #Z (n - 1))) * (diff (cos,x)) by TAYLOR_1:3
.= (n * ((cos . x) #Z (n - 1))) * (- (sin . x)) by SIN_COS:63
.= - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) ;
assume  x in Z ; ::_thesis: (((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x))
hence  (((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) by A15, A17, FDIFF_1:def_7; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(((sin_*_f)_(#)_((#Z_n)_*_cos))_`|_Z)_._x_=_(n_*_((cos_._x)_#Z_(n_-_1)))_*_(cos_._((n_+_1)_*_x))
let x be Real; ::_thesis: ( x in Z implies (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) )
A18: n - 1 is Element of NAT by A2, NAT_1:21;
assume A19: x in Z ; ::_thesis: (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x))
then (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = ((((#Z n) * cos) . x) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * cos),x))) by A1, A10, A15, FDIFF_1:21
.= (((#Z n) . (cos . x)) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * cos),x))) by A14, A19, FUNCT_1:12
.= (((cos . x) #Z n) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * cos),x))) by TAYLOR_1:def_1
.= (((cos . x) #Z n) * (((sin * f) `| Z) . x)) + (((sin * f) . x) * (diff (((#Z n) * cos),x))) by A10, A19, FDIFF_1:def_7
.= (((cos . x) #Z n) * (n * (cos . (n * x)))) + (((sin * f) . x) * (diff (((#Z n) * cos),x))) by A11, A19
.= (((cos . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (f . x)) * (diff (((#Z n) * cos),x))) by A6, A19, FUNCT_1:12
.= (((cos . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * (diff (((#Z n) * cos),x))) by A3, A19
.= (((cos . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * ((((#Z n) * cos) `| Z) . x)) by A15, A19, FDIFF_1:def_7
.= (((cos . x) #Z ((n - 1) + 1)) * (n * (cos . (n * x)))) + ((sin . (n * x)) * (- ((n * ((cos . x) #Z (n - 1))) * (sin . x)))) by A16, A19
.= ((((cos . x) #Z (n - 1)) * ((cos . x) #Z 1)) * (n * (cos . (n * x)))) + ((sin . (n * x)) * (- ((n * ((cos . x) #Z (n - 1))) * (sin . x)))) by A18, TAYLOR_1:1
.= ((((cos . x) #Z (n - 1)) * ((cos . x) #Z 1)) * (n * (cos . (n * x)))) - ((((sin . (n * x)) * n) * ((cos . x) #Z (n - 1))) * (sin . x))
.= ((((cos . x) #Z (n - 1)) * (cos . x)) * (n * (cos . (n * x)))) - ((((sin . (n * x)) * n) * ((cos . x) #Z (n - 1))) * (sin . x)) by PREPOWER:35
.= (n * ((cos . x) #Z (n - 1))) * (((cos . (n * x)) * (cos . x)) - ((sin . x) * (sin . (n * x))))
.= (n * ((cos . x) #Z (n - 1))) * (cos . (x + (n * x))) by SIN_COS:74
.= (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ;
hence  (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ; ::_thesis: verum
end;
hence  ( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) by A1, A10, A15, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_5:14
for Z being open Subset of REAL st not 0 in Z & Z c= dom (((id Z) ^) (#) sin) holds
( ((id Z) ^) (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) sin) `| Z) . x = ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & Z c= dom (((id Z) ^) (#) sin) implies ( ((id Z) ^) (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) sin) `| Z) . x = ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) ) ) )
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (((id Z) ^) (#) sin) ; ::_thesis: ( ((id Z) ^) (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) sin) `| Z) . x = ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) ) )
A3: (id Z) ^ is_differentiable_on Z by A1, Th4;
A4: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;
 Z c= (dom ((id Z) ^)) /\ (dom sin) by A2, VALUED_1:def_4;
then A5: Z c= dom ((id Z) ^) by XBOOLE_1:18;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
((((id_Z)_^)_(#)_sin)_`|_Z)_._x_=_((1_/_x)_*_(cos_._x))_-_((1_/_(x_^2))_*_(sin_._x))
let x be Real; ::_thesis: ( x in Z implies ((((id Z) ^) (#) sin) `| Z) . x = ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) )
assume A6: x in Z ; ::_thesis: ((((id Z) ^) (#) sin) `| Z) . x = ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x))
hence ((((id Z) ^) (#) sin) `| Z) . x = ((sin . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff (sin,x))) by A2, A3, A4, FDIFF_1:21
.= ((sin . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff (sin,x))) by A3, A6, FDIFF_1:def_7
.= ((sin . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff (sin,x))) by A1, A6, Th4
.= ((sin . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (cos . x)) by SIN_COS:64
.= ((sin . x) * (- (1 / (x ^2)))) + ((((id Z) . x) ") * (cos . x)) by A5, A6, RFUNCT_1:def_2
.= ((sin . x) * (- (1 / (x ^2)))) + ((1 * (x ")) * (cos . x)) by A6, FUNCT_1:18
.= (- ((1 / (x ^2)) * (sin . x))) + ((1 / x) * (cos . x)) by XCMPLX_0:def_9
.= ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) ;
::_thesis: verum
end;
hence  ( ((id Z) ^) (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) sin) `| Z) . x = ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) ) ) by A2, A3, A4, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_5:15
for Z being open Subset of REAL st not 0 in Z & Z c= dom (((id Z) ^) (#) cos) holds
( ((id Z) ^) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) cos) `| Z) . x = (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & Z c= dom (((id Z) ^) (#) cos) implies ( ((id Z) ^) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) cos) `| Z) . x = (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x)) ) ) )
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (((id Z) ^) (#) cos) ; ::_thesis: ( ((id Z) ^) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) cos) `| Z) . x = (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x)) ) )
A3: (id Z) ^ is_differentiable_on Z by A1, Th4;
A4: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67;
 Z c= (dom ((id Z) ^)) /\ (dom cos) by A2, VALUED_1:def_4;
then A5: Z c= dom ((id Z) ^) by XBOOLE_1:18;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
((((id_Z)_^)_(#)_cos)_`|_Z)_._x_=_(-_((1_/_x)_*_(sin_._x)))_-_((1_/_(x_^2))_*_(cos_._x))
let x be Real; ::_thesis: ( x in Z implies ((((id Z) ^) (#) cos) `| Z) . x = (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x)) )
assume A6: x in Z ; ::_thesis: ((((id Z) ^) (#) cos) `| Z) . x = (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x))
hence ((((id Z) ^) (#) cos) `| Z) . x = ((cos . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff (cos,x))) by A2, A3, A4, FDIFF_1:21
.= ((cos . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff (cos,x))) by A3, A6, FDIFF_1:def_7
.= ((cos . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff (cos,x))) by A1, A6, Th4
.= ((cos . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (- (sin . x))) by SIN_COS:63
.= ((cos . x) * (- (1 / (x ^2)))) + ((((id Z) . x) ") * (- (sin . x))) by A5, A6, RFUNCT_1:def_2
.= ((cos . x) * (- (1 / (x ^2)))) + ((1 * (x ")) * (- (sin . x))) by A6, FUNCT_1:18
.= (- ((1 / (x ^2)) * (cos . x))) + ((1 / x) * (- (sin . x))) by XCMPLX_0:def_9
.= (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x)) ;
::_thesis: verum
end;
hence  ( ((id Z) ^) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) cos) `| Z) . x = (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x)) ) ) by A2, A3, A4, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_5:16
for Z being open Subset of REAL st Z c= dom (sin + (#R (1 / 2))) holds
( sin + (#R (1 / 2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin + (#R (1 / 2))) implies ( sin + (#R (1 / 2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ) ) )
assume A1: Z c= dom (sin + (#R (1 / 2))) ; ::_thesis: ( sin + (#R (1 / 2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ) )
then  Z c= (dom (#R (1 / 2))) /\ (dom sin) by VALUED_1:def_1;
then A2: Z c= dom (#R (1 / 2)) by XBOOLE_1:18;
then A3: #R (1 / 2) is_differentiable_on Z by Lm3;
A4: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
((sin_+_(#R_(1_/_2)))_`|_Z)_._x_=_(cos_._x)_+_((1_/_2)_*_(x_#R_(-_(1_/_2))))
let x be Real; ::_thesis: ( x in Z implies ((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) )
assume A5: x in Z ; ::_thesis: ((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2))))
then ((sin + (#R (1 / 2))) `| Z) . x = (diff (sin,x)) + (diff ((#R (1 / 2)),x)) by A1, A3, A4, FDIFF_1:18
.= (cos . x) + (diff ((#R (1 / 2)),x)) by SIN_COS:64
.= (cos . x) + (((#R (1 / 2)) `| Z) . x) by A3, A5, FDIFF_1:def_7
.= (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) by A2, A5, Lm3 ;
hence  ((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ; ::_thesis: verum
end;
hence  ( sin + (#R (1 / 2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ) ) by A1, A3, A4, FDIFF_1:18; ::_thesis: verum
end;

theorem :: FDIFF_5:17
for Z being open Subset of REAL
for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (sin * ((id Z) ^))) & g = #Z 2 holds
( g (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (sin * ((id Z) ^))) & g = #Z 2 holds
( g (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ) )
let g be PartFunc of REAL,REAL; ::_thesis: ( not 0 in Z & Z c= dom (g (#) (sin * ((id Z) ^))) & g = #Z 2 implies ( g (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ) ) )
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (g (#) (sin * ((id Z) ^))) and
A3: g = #Z 2 ; ::_thesis: ( g (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ) )
A4: for x being Real st x in Z holds
g is_differentiable_in x by A3, TAYLOR_1:2;
A5: Z c= (dom g) /\ (dom (sin * ((id Z) ^))) by A2, VALUED_1:def_4;
then  Z c= dom g by XBOOLE_1:18;
then A6: g is_differentiable_on Z by A4, FDIFF_1:9;
A7: for x being Real st x in Z holds
(g `| Z) . x = 2 * x
proof
let x be Real; ::_thesis: ( x in Z implies (g `| Z) . x = 2 * x )
assume A8: x in Z ; ::_thesis: (g `| Z) . x = 2 * x
diff (g,x) = 2 * (x #Z (2 - 1)) by A3, TAYLOR_1:2
.= 2 * x by PREPOWER:35 ;
hence  (g `| Z) . x = 2 * x by A6, A8, FDIFF_1:def_7; ::_thesis: verum
end;
A9: sin * ((id Z) ^) is_differentiable_on Z by A1, Th5;
A10: Z c= dom (sin * ((id Z) ^)) by A5, XBOOLE_1:18;
then  for y being set st y in Z holds
y in dom ((id Z) ^) by FUNCT_1:11;
then A11: Z c= dom ((id Z) ^) by TARSKI:def_3;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
((g_(#)_(sin_*_((id_Z)_^)))_`|_Z)_._x_=_((2_*_x)_*_(sin_._(1_/_x)))_-_(cos_._(1_/_x))
let x be Real; ::_thesis: ( x in Z implies ((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) )
assume A12: x in Z ; ::_thesis: ((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x))
then ((g (#) (sin * ((id Z) ^))) `| Z) . x = (((sin * ((id Z) ^)) . x) * (diff (g,x))) + ((g . x) * (diff ((sin * ((id Z) ^)),x))) by A2, A9, A6, FDIFF_1:21
.= (((sin * ((id Z) ^)) . x) * ((g `| Z) . x)) + ((g . x) * (diff ((sin * ((id Z) ^)),x))) by A6, A12, FDIFF_1:def_7
.= (((sin * ((id Z) ^)) . x) * (2 * x)) + ((g . x) * (diff ((sin * ((id Z) ^)),x))) by A7, A12
.= (((sin * ((id Z) ^)) . x) * (2 * x)) + ((x #Z 2) * (diff ((sin * ((id Z) ^)),x))) by A3, TAYLOR_1:def_1
.= (((sin * ((id Z) ^)) . x) * (2 * x)) + ((x #Z 2) * (((sin * ((id Z) ^)) `| Z) . x)) by A9, A12, FDIFF_1:def_7
.= (((sin * ((id Z) ^)) . x) * (2 * x)) + ((x #Z 2) * (- ((1 / (x ^2)) * (cos . (1 / x))))) by A1, A12, Th5
.= (((sin * ((id Z) ^)) . x) * (2 * x)) - ((x #Z (1 + 1)) * ((1 / (x ^2)) * (cos . (1 / x))))
.= (((sin * ((id Z) ^)) . x) * (2 * x)) - (((x #Z 1) * (x #Z 1)) * ((1 / (x ^2)) * (cos . (1 / x)))) by TAYLOR_1:1
.= (((sin * ((id Z) ^)) . x) * (2 * x)) - ((x * (x #Z 1)) * ((1 / (x ^2)) * (cos . (1 / x)))) by PREPOWER:35
.= (((sin * ((id Z) ^)) . x) * (2 * x)) - ((x * x) * (((1 * 1) / (x * x)) * (cos . (1 / x)))) by PREPOWER:35
.= (((sin * ((id Z) ^)) . x) * (2 * x)) - ((x * x) * (((1 / x) * (1 / x)) * (cos . (1 / x)))) by XCMPLX_1:102
.= (((sin * ((id Z) ^)) . x) * (2 * x)) - (((x * (1 / x)) * (x * (1 / x))) * (cos . (1 / x)))
.= (((sin * ((id Z) ^)) . x) * (2 * x)) - (((x * (1 / x)) * 1) * (cos . (1 / x))) by A1, A12, XCMPLX_1:106
.= (((sin * ((id Z) ^)) . x) * (2 * x)) - ((1 * 1) * (cos . (1 / x))) by A1, A12, XCMPLX_1:106
.= ((sin . (((id Z) ^) . x)) * (2 * x)) - (cos . (1 / x)) by A10, A12, FUNCT_1:12
.= ((sin . (((id Z) . x) ")) * (2 * x)) - (cos . (1 / x)) by A11, A12, RFUNCT_1:def_2
.= ((sin . (1 * (x "))) * (2 * x)) - (cos . (1 / x)) by A12, FUNCT_1:18
.= ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) by XCMPLX_0:def_9 ;
hence  ((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ; ::_thesis: verum
end;
hence  ( g (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ) ) by A2, A9, A6, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_5:18
for Z being open Subset of REAL
for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (cos * ((id Z) ^))) & g = #Z 2 holds
( g (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (cos * ((id Z) ^))) & g = #Z 2 holds
( g (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ) )
let g be PartFunc of REAL,REAL; ::_thesis: ( not 0 in Z & Z c= dom (g (#) (cos * ((id Z) ^))) & g = #Z 2 implies ( g (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ) ) )
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (g (#) (cos * ((id Z) ^))) and
A3: g = #Z 2 ; ::_thesis: ( g (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ) )
A4: for x being Real st x in Z holds
g is_differentiable_in x by A3, TAYLOR_1:2;
A5: Z c= (dom g) /\ (dom (cos * ((id Z) ^))) by A2, VALUED_1:def_4;
then A6: Z c= dom (cos * ((id Z) ^)) by XBOOLE_1:18;
then A7: cos * ((id Z) ^) is_differentiable_on Z by A1, Th6;
 Z c= dom g by A5, XBOOLE_1:18;
then A8: g is_differentiable_on Z by A4, FDIFF_1:9;
A9: for x being Real st x in Z holds
(g `| Z) . x = 2 * x
proof
let x be Real; ::_thesis: ( x in Z implies (g `| Z) . x = 2 * x )
assume A10: x in Z ; ::_thesis: (g `| Z) . x = 2 * x
diff (g,x) = 2 * (x #Z (2 - 1)) by A3, TAYLOR_1:2
.= 2 * x by PREPOWER:35 ;
hence  (g `| Z) . x = 2 * x by A8, A10, FDIFF_1:def_7; ::_thesis: verum
end;
 for y being set st y in Z holds
y in dom ((id Z) ^) by A6, FUNCT_1:11;
then A11: Z c= dom ((id Z) ^) by TARSKI:def_3;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
((g_(#)_(cos_*_((id_Z)_^)))_`|_Z)_._x_=_((2_*_x)_*_(cos_._(1_/_x)))_+_(sin_._(1_/_x))
let x be Real; ::_thesis: ( x in Z implies ((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) )
assume A12: x in Z ; ::_thesis: ((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x))
then ((g (#) (cos * ((id Z) ^))) `| Z) . x = (((cos * ((id Z) ^)) . x) * (diff (g,x))) + ((g . x) * (diff ((cos * ((id Z) ^)),x))) by A2, A7, A8, FDIFF_1:21
.= (((cos * ((id Z) ^)) . x) * ((g `| Z) . x)) + ((g . x) * (diff ((cos * ((id Z) ^)),x))) by A8, A12, FDIFF_1:def_7
.= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((g . x) * (diff ((cos * ((id Z) ^)),x))) by A9, A12
.= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((x #Z 2) * (diff ((cos * ((id Z) ^)),x))) by A3, TAYLOR_1:def_1
.= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((x #Z 2) * (((cos * ((id Z) ^)) `| Z) . x)) by A7, A12, FDIFF_1:def_7
.= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((x #Z (1 + 1)) * ((1 / (x ^2)) * (sin . (1 / x)))) by A1, A6, A12, Th6
.= (((cos * ((id Z) ^)) . x) * (2 * x)) + (((x #Z 1) * (x #Z 1)) * ((1 / (x ^2)) * (sin . (1 / x)))) by TAYLOR_1:1
.= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((x * (x #Z 1)) * ((1 / (x ^2)) * (sin . (1 / x)))) by PREPOWER:35
.= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((x * x) * (((1 * 1) / (x * x)) * (sin . (1 / x)))) by PREPOWER:35
.= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((x * x) * (((1 / x) * (1 / x)) * (sin . (1 / x)))) by XCMPLX_1:102
.= (((cos * ((id Z) ^)) . x) * (2 * x)) + (((x * (1 / x)) * (x * (1 / x))) * (sin . (1 / x)))
.= (((cos * ((id Z) ^)) . x) * (2 * x)) + (((x * (1 / x)) * 1) * (sin . (1 / x))) by A1, A12, XCMPLX_1:106
.= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((1 * 1) * (sin . (1 / x))) by A1, A12, XCMPLX_1:106
.= ((cos . (((id Z) ^) . x)) * (2 * x)) + (sin . (1 / x)) by A6, A12, FUNCT_1:12
.= ((cos . (((id Z) . x) ")) * (2 * x)) + (sin . (1 / x)) by A11, A12, RFUNCT_1:def_2
.= ((cos . (1 * (x "))) * (2 * x)) + (sin . (1 / x)) by A12, FUNCT_1:18
.= ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) by XCMPLX_0:def_9 ;
hence  ((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ; ::_thesis: verum
end;
hence  ( g (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ) ) by A2, A7, A8, FDIFF_1:21; ::_thesis: verum
end;

Lm5:  for x being Real st x in dom ln holds
x > 0
by TAYLOR_1:18, XXREAL_1:4;

theorem Th19: :: FDIFF_5:19
for Z being open Subset of REAL st Z c= dom ln holds
( ln is_differentiable_on Z & ( for x being Real st x in Z holds
(ln `| Z) . x = 1 / x ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom ln implies ( ln is_differentiable_on Z & ( for x being Real st x in Z holds
(ln `| Z) . x = 1 / x ) ) )
assume A1: Z c= dom ln ; ::_thesis: ( ln is_differentiable_on Z & ( for x being Real st x in Z holds
(ln `| Z) . x = 1 / x ) )
then A2: for x being Real st x in Z holds
ln is_differentiable_in x by Lm5, TAYLOR_1:18;
then A3: ln is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
(ln `| Z) . x = 1 / x
proof
let x be Real; ::_thesis: ( x in Z implies (ln `| Z) . x = 1 / x )
assume A4: x in Z ; ::_thesis: (ln `| Z) . x = 1 / x
then  diff (ln,x) = 1 / x by A1, TAYLOR_1:18;
hence  (ln `| Z) . x = 1 / x by A3, A4, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( ln is_differentiable_on Z & ( for x being Real st x in Z holds
(ln `| Z) . x = 1 / x ) ) by A1, A2, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_5:20
for Z being open Subset of REAL st Z c= dom ((id Z) (#) ln) holds
( (id Z) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((id Z) (#) ln) implies ( (id Z) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ) ) )
set f = ln ;
assume A1: Z c= dom ((id Z) (#) ln) ; ::_thesis: ( (id Z) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ) )
then A2: Z c= (dom (id Z)) /\ (dom ln) by VALUED_1:def_4;
then A3: Z c= dom (id Z) by XBOOLE_1:18;
A4: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:18;
then A5: id Z is_differentiable_on Z by A3, FDIFF_1:23;
A6: Z c= dom ln by A2, XBOOLE_1:18;
then A7: ln is_differentiable_on Z by Th19;
 for x being Real st x in Z holds
(((id Z) (#) ln) `| Z) . x = 1 + (ln . x)
proof
let x be Real; ::_thesis: ( x in Z implies (((id Z) (#) ln) `| Z) . x = 1 + (ln . x) )
assume A8: x in Z ; ::_thesis: (((id Z) (#) ln) `| Z) . x = 1 + (ln . x)
then A9: x <> 0 by A6, TAYLOR_1:18, XXREAL_1:4;
(((id Z) (#) ln) `| Z) . x = (((id Z) . x) * (diff (ln,x))) + ((ln . x) * (diff ((id Z),x))) by A1, A5, A7, A8, FDIFF_1:21
.= (((id Z) . x) * ((ln `| Z) . x)) + ((ln . x) * (diff ((id Z),x))) by A7, A8, FDIFF_1:def_7
.= (((id Z) . x) * (1 / x)) + ((ln . x) * (diff ((id Z),x))) by A6, A8, Th19
.= (x * (1 / x)) + ((ln . x) * (diff ((id Z),x))) by A8, FUNCT_1:18
.= (x * (1 / x)) + ((ln . x) * (((id Z) `| Z) . x)) by A5, A8, FDIFF_1:def_7
.= (x * (1 / x)) + ((ln . x) * 1) by A3, A4, A8, FDIFF_1:23
.= 1 + (ln . x) by A9, XCMPLX_1:106 ;
hence  (((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ; ::_thesis: verum
end;
hence  ( (id Z) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ) ) by A1, A5, A7, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_5:21
for Z being open Subset of REAL
for g being PartFunc of REAL,REAL st Z c= dom (g (#) ln) & g = #Z 2 & ( for x being Real st x in Z holds
x > 0 ) holds
( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: for g being PartFunc of REAL,REAL st Z c= dom (g (#) ln) & g = #Z 2 & ( for x being Real st x in Z holds
x > 0 ) holds
( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) )
let g be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (g (#) ln) & g = #Z 2 & ( for x being Real st x in Z holds
x > 0 ) implies ( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) ) )
set f = ln ;
assume that
A1: Z c= dom (g (#) ln) and
A2: g = #Z 2 and
A3: for x being Real st x in Z holds
x > 0 ; ::_thesis: ( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) )
A4: for x being Real st x in Z holds
g is_differentiable_in x by A2, TAYLOR_1:2;
A5: Z c= (dom g) /\ (dom ln) by A1, VALUED_1:def_4;
then A6: Z c= dom ln by XBOOLE_1:18;
then A7: ln is_differentiable_on Z by Th19;
 Z c= dom g by A5, XBOOLE_1:18;
then A8: g is_differentiable_on Z by A4, FDIFF_1:9;
A9: for x being Real st x in Z holds
(g `| Z) . x = 2 * x
proof
let x be Real; ::_thesis: ( x in Z implies (g `| Z) . x = 2 * x )
assume A10: x in Z ; ::_thesis: (g `| Z) . x = 2 * x
diff (g,x) = 2 * (x #Z (2 - 1)) by A2, TAYLOR_1:2
.= 2 * x by PREPOWER:35 ;
hence  (g `| Z) . x = 2 * x by A8, A10, FDIFF_1:def_7; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
((g_(#)_ln)_`|_Z)_._x_=_x_+_((2_*_x)_*_(ln_._x))
let x be Real; ::_thesis: ( x in Z implies ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) )
assume A11: x in Z ; ::_thesis: ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x))
then A12: x <> 0 by A3;
((g (#) ln) `| Z) . x = ((g . x) * (diff (ln,x))) + ((ln . x) * (diff (g,x))) by A1, A8, A7, A11, FDIFF_1:21
.= ((g . x) * ((ln `| Z) . x)) + ((ln . x) * (diff (g,x))) by A7, A11, FDIFF_1:def_7
.= ((g . x) * (1 / x)) + ((ln . x) * (diff (g,x))) by A6, A11, Th19
.= ((x #Z 2) * (1 / x)) + ((ln . x) * (diff (g,x))) by A2, TAYLOR_1:def_1
.= ((x #Z 2) * (1 / x)) + ((ln . x) * ((g `| Z) . x)) by A8, A11, FDIFF_1:def_7
.= ((x #Z (1 + 1)) * (1 / x)) + ((2 * x) * (ln . x)) by A9, A11
.= (((x #Z 1) * (x #Z 1)) * (1 / x)) + ((2 * x) * (ln . x)) by TAYLOR_1:1
.= (((x #Z 1) * x) * (1 / x)) + ((2 * x) * (ln . x)) by PREPOWER:35
.= ((x * x) * (1 / x)) + ((2 * x) * (ln . x)) by PREPOWER:35
.= (x * (x * (1 / x))) + ((2 * x) * (ln . x))
.= (x * 1) + ((2 * x) * (ln . x)) by A12, XCMPLX_1:106
.= x + ((2 * x) * (ln . x)) ;
hence  ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ; ::_thesis: verum
end;
hence  ( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) ) by A1, A8, A7, FDIFF_1:21; ::_thesis: verum
end;

theorem Th22: :: FDIFF_5:22
for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom ((f1 + f2) / (f1 - f2)) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) holds
( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) )
proof
let a be Real; ::_thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom ((f1 + f2) / (f1 - f2)) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) holds
( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) )
let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom ((f1 + f2) / (f1 - f2)) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) holds
( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((f1 + f2) / (f1 - f2)) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) implies ( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) ) )
assume that
A1: Z c= dom ((f1 + f2) / (f1 - f2)) and
A2: for x being Real st x in Z holds
f1 . x = a and
A3: f2 = #Z 2 and
A4: for x being Real st x in Z holds
(f1 - f2) . x > 0 ; ::_thesis: ( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) )
A5: Z c= (dom (f1 + f2)) /\ ((dom (f1 - f2)) \ ((f1 - f2) " {0})) by A1, RFUNCT_1:def_1;
then A6: Z c= dom (f1 + f2) by XBOOLE_1:18;
then A7: f1 + f2 is_differentiable_on Z by A2, A3, Lm1;
A8: Z c= dom (f1 - f2) by A5, XBOOLE_1:1;
then A9: f1 - f2 is_differentiable_on Z by A2, A3, Lm2;
A10: for x being Real st x in Z holds
(f1 - f2) . x <> 0 by A4;
then A11: (f1 + f2) / (f1 - f2) is_differentiable_on Z by A7, A9, FDIFF_2:21;
 for x being Real st x in Z holds
(((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2)
proof
let x be Real; ::_thesis: ( x in Z implies (((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) )
assume A12: x in Z ; ::_thesis: (((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2)
then A13: f1 . x = a by A2;
A14: (f1 - f2) . x <> 0 by A4, A12;
 ( f1 + f2 is_differentiable_in x & f1 - f2 is_differentiable_in x ) by A7, A9, A12, FDIFF_1:9;
then  diff (((f1 + f2) / (f1 - f2)),x) = (((diff ((f1 + f2),x)) * ((f1 - f2) . x)) - ((diff ((f1 - f2),x)) * ((f1 + f2) . x))) / (((f1 - f2) . x) ^2) by A14, FDIFF_2:14
.= (((diff ((f1 + f2),x)) * ((f1 . x) - (f2 . x))) - ((diff ((f1 - f2),x)) * ((f1 + f2) . x))) / (((f1 - f2) . x) ^2) by A8, A12, VALUED_1:13
.= (((diff ((f1 + f2),x)) * ((f1 . x) - (f2 . x))) - ((diff ((f1 - f2),x)) * ((f1 . x) + (f2 . x)))) / (((f1 - f2) . x) ^2) by A6, A12, VALUED_1:def_1
.= (((diff ((f1 + f2),x)) * ((f1 . x) - (f2 . x))) - ((diff ((f1 - f2),x)) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2) by A8, A12, VALUED_1:13
.= (((((f1 + f2) `| Z) . x) * ((f1 . x) - (f2 . x))) - ((diff ((f1 - f2),x)) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2) by A7, A12, FDIFF_1:def_7
.= (((2 * x) * ((f1 . x) - (f2 . x))) - ((diff ((f1 - f2),x)) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2) by A2, A3, A6, A12, Lm1
.= (((2 * x) * ((f1 . x) - (f2 . x))) - ((((f1 - f2) `| Z) . x) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2) by A9, A12, FDIFF_1:def_7
.= (((2 * x) * ((f1 . x) - (f2 . x))) - ((- (2 * x)) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2) by A2, A3, A8, A12, Lm2
.= ((4 * x) * a) / ((a - (x #Z 2)) ^2) by A3, A13, TAYLOR_1:def_1
.= ((4 * x) * a) / ((a - (x |^ 2)) ^2) by PREPOWER:36
.= ((4 * x) * a) / (((a - (x |^ 2)) |^ 1) * (a - (x |^ 2))) by NEWTON:5
.= ((4 * x) * a) / ((a - (x |^ 2)) |^ (1 + 1)) by NEWTON:6
.= ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ;
hence  (((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) by A11, A12, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) ) by A7, A9, A10, FDIFF_2:21; ::_thesis: verum
end;

theorem :: FDIFF_5:23
for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * ((f1 + f2) / (f1 - f2))) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) & ( for x being Real st x in Z holds
(f1 + f2) . x > 0 ) holds
( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) )
proof
let a be Real; ::_thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * ((f1 + f2) / (f1 - f2))) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) & ( for x being Real st x in Z holds
(f1 + f2) . x > 0 ) holds
( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) )
let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * ((f1 + f2) / (f1 - f2))) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) & ( for x being Real st x in Z holds
(f1 + f2) . x > 0 ) holds
( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (ln * ((f1 + f2) / (f1 - f2))) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) & ( for x being Real st x in Z holds
(f1 + f2) . x > 0 ) implies ( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) ) )
assume that
A1: Z c= dom (ln * ((f1 + f2) / (f1 - f2))) and
A2: for x being Real st x in Z holds
f1 . x = a and
A3: f2 = #Z 2 and
A4: for x being Real st x in Z holds
(f1 - f2) . x > 0 and
A5: for x being Real st x in Z holds
(f1 + f2) . x > 0 ; ::_thesis: ( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) )
 for y being set st y in Z holds
y in dom ((f1 + f2) / (f1 - f2)) by A1, FUNCT_1:11;
then A6: Z c= dom ((f1 + f2) / (f1 - f2)) by TARSKI:def_3;
then A7: (f1 + f2) / (f1 - f2) is_differentiable_on Z by A2, A3, A4, Th22;
A8: Z c= (dom (f1 + f2)) /\ ((dom (f1 - f2)) \ ((f1 - f2) " {0})) by A6, RFUNCT_1:def_1;
then A9: Z c= dom (f1 + f2) by XBOOLE_1:18;
A10: Z c= dom (f1 - f2) by A8, XBOOLE_1:1;
A11: for x being Real st x in Z holds
((f1 + f2) / (f1 - f2)) . x > 0
proof
let x be Real; ::_thesis: ( x in Z implies ((f1 + f2) / (f1 - f2)) . x > 0 )
assume A12: x in Z ; ::_thesis: ((f1 + f2) / (f1 - f2)) . x > 0
then  x in dom ((f1 + f2) / (f1 - f2)) by A1, FUNCT_1:11;
then A13: ((f1 + f2) / (f1 - f2)) . x = ((f1 + f2) . x) * (((f1 - f2) . x) ") by RFUNCT_1:def_1
.= ((f1 + f2) . x) / ((f1 - f2) . x) by XCMPLX_0:def_9 ;
 ( (f1 + f2) . x > 0 & (f1 - f2) . x > 0 ) by A4, A5, A12;
hence  ((f1 + f2) / (f1 - f2)) . x > 0 by A13, XREAL_1:139; ::_thesis: verum
end;
A14: for x being Real st x in Z holds
ln * ((f1 + f2) / (f1 - f2)) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies ln * ((f1 + f2) / (f1 - f2)) is_differentiable_in x )
assume  x in Z ; ::_thesis: ln * ((f1 + f2) / (f1 - f2)) is_differentiable_in x
then  ( (f1 + f2) / (f1 - f2) is_differentiable_in x & ((f1 + f2) / (f1 - f2)) . x > 0 ) by A7, A11, FDIFF_1:9;
hence  ln * ((f1 + f2) / (f1 - f2)) is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum
end;
then A15: ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4))
proof
let x be Real; ::_thesis: ( x in Z implies ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) )
assume A16: x in Z ; ::_thesis: ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4))
then A17: x in dom ((f1 + f2) / (f1 - f2)) by A1, FUNCT_1:11;
A18: (f1 - f2) . x <> 0 by A4, A16;
A19: f1 . x = a by A2, A16;
 ( (f1 + f2) / (f1 - f2) is_differentiable_in x & ((f1 + f2) / (f1 - f2)) . x > 0 ) by A7, A11, A16, FDIFF_1:9;
then  diff ((ln * ((f1 + f2) / (f1 - f2))),x) = (diff (((f1 + f2) / (f1 - f2)),x)) / (((f1 + f2) / (f1 - f2)) . x) by TAYLOR_1:20
.= ((((f1 + f2) / (f1 - f2)) `| Z) . x) / (((f1 + f2) / (f1 - f2)) . x) by A7, A16, FDIFF_1:def_7
.= ((((f1 + f2) / (f1 - f2)) `| Z) . x) / (((f1 + f2) . x) * (((f1 - f2) . x) ")) by A17, RFUNCT_1:def_1
.= (((4 * a) * x) / (((f1 . x) - (x |^ 2)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) ")) by A2, A3, A4, A6, A16, A19, Th22
.= (((4 * a) * x) / (((f1 . x) - (x #Z 2)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) ")) by PREPOWER:36
.= (((4 * a) * x) / (((f1 . x) - (f2 . x)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) ")) by A3, TAYLOR_1:def_1
.= (((4 * a) * x) / (((f1 - f2) . x) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) ")) by A10, A16, VALUED_1:13
.= (((4 * a) * x) / (((f1 - f2) . x) |^ (1 + 1))) / (((f1 + f2) . x) / ((f1 - f2) . x)) by XCMPLX_0:def_9
.= (((4 * a) * x) / ((((f1 - f2) . x) |^ 1) * ((f1 - f2) . x))) / (((f1 + f2) . x) / ((f1 - f2) . x)) by NEWTON:6
.= (((4 * a) * x) / (((f1 - f2) . x) * ((f1 - f2) . x))) / (((f1 + f2) . x) / ((f1 - f2) . x)) by NEWTON:5
.= ((((4 * a) * x) / ((f1 - f2) . x)) / ((f1 - f2) . x)) / (((f1 + f2) . x) / ((f1 - f2) . x)) by XCMPLX_1:78
.= ((((4 * a) * x) / ((f1 - f2) . x)) / (((f1 + f2) . x) / ((f1 - f2) . x))) / ((f1 - f2) . x) by XCMPLX_1:48
.= (((4 * a) * x) / ((f1 + f2) . x)) / ((f1 - f2) . x) by A18, XCMPLX_1:55
.= ((4 * a) * x) / (((f1 + f2) . x) * ((f1 - f2) . x)) by XCMPLX_1:78
.= ((4 * a) * x) / (((f1 . x) + (f2 . x)) * ((f1 - f2) . x)) by A9, A16, VALUED_1:def_1
.= ((4 * a) * x) / (((f1 . x) + (f2 . x)) * ((f1 . x) - (f2 . x))) by A10, A16, VALUED_1:13
.= ((4 * a) * x) / ((a * a) - ((f2 . x) * (f2 . x))) by A19
.= ((4 * a) * x) / ((a * a) - ((x #Z 2) * (f2 . x))) by A3, TAYLOR_1:def_1
.= ((4 * a) * x) / ((a * a) - ((x #Z 2) * (x #Z 2))) by A3, TAYLOR_1:def_1
.= ((4 * a) * x) / (((a |^ 1) * a) - ((x #Z 2) * (x #Z 2))) by NEWTON:5
.= ((4 * a) * x) / ((a |^ (1 + 1)) - ((x #Z 2) * (x #Z 2))) by NEWTON:6
.= ((4 * a) * x) / ((a |^ (1 + 1)) - ((x |^ 2) * (x #Z 2))) by PREPOWER:36
.= ((4 * a) * x) / ((a |^ 2) - ((x |^ 2) * (x |^ 2))) by PREPOWER:36
.= ((4 * a) * x) / ((a |^ 2) - (x |^ (2 + 2))) by NEWTON:8
.= ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ;
hence  ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) by A15, A16, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) ) by A1, A14, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_5:24
for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) ln) & ( for x being Real st x in Z holds
x > 0 ) holds
( ((id Z) ^) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (((id Z) ^) (#) ln) & ( for x being Real st x in Z holds
x > 0 ) implies ( ((id Z) ^) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) ) ) )
set f = id Z;
set g = ln ;
assume that
A1: Z c= dom (((id Z) ^) (#) ln) and
A2: for x being Real st x in Z holds
x > 0 ; ::_thesis: ( ((id Z) ^) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) ) )
A3: not 0 in Z by A2;
then A4: (id Z) ^ is_differentiable_on Z by Th4;
A5: Z c= (dom ((id Z) ^)) /\ (dom ln) by A1, VALUED_1:def_4;
then A6: Z c= dom ln by XBOOLE_1:18;
then A7: ln is_differentiable_on Z by Th19;
A8: Z c= dom ((id Z) ^) by A5, XBOOLE_1:18;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
((((id_Z)_^)_(#)_ln)_`|_Z)_._x_=_(1_/_(x_^2))_*_(1_-_(ln_._x))
let x be Real; ::_thesis: ( x in Z implies ((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) )
assume A9: x in Z ; ::_thesis: ((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x))
then ((((id Z) ^) (#) ln) `| Z) . x = ((ln . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff (ln,x))) by A1, A4, A7, FDIFF_1:21
.= ((ln . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff (ln,x))) by A4, A9, FDIFF_1:def_7
.= ((ln . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff (ln,x))) by A3, A9, Th4
.= ((ln . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * ((ln `| Z) . x)) by A7, A9, FDIFF_1:def_7
.= ((ln . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (1 / x)) by A6, A9, Th19
.= ((ln . x) * (- (1 / (x ^2)))) + ((((id Z) . x) ") * (1 / x)) by A8, A9, RFUNCT_1:def_2
.= ((ln . x) * (- (1 / (x ^2)))) + ((1 * (x ")) * (1 / x)) by A9, FUNCT_1:18
.= (- ((1 / (x ^2)) * (ln . x))) + ((1 / x) * (1 / x)) by XCMPLX_0:def_9
.= (- ((1 / (x ^2)) * (ln . x))) + (1 / (x ^2)) by XCMPLX_1:102
.= (1 / (x ^2)) * (1 - (ln . x)) ;
hence  ((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) ; ::_thesis: verum
end;
hence  ( ((id Z) ^) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) ) ) by A1, A4, A7, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_5:25
for Z being open Subset of REAL st Z c= dom (ln ^) & ( for x being Real st x in Z holds
ln . x <> 0 ) holds
( ln ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln ^) & ( for x being Real st x in Z holds
ln . x <> 0 ) implies ( ln ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) ) ) )
set f = ln ;
assume that
A1: Z c= dom (ln ^) and
A2: for x being Real st x in Z holds
ln . x <> 0 ; ::_thesis: ( ln ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) ) )
 dom (ln ^) c= dom ln by RFUNCT_1:1;
then A3: Z c= dom ln by A1, XBOOLE_1:1;
then A4: ln is_differentiable_on Z by Th19;
then A5: ln ^ is_differentiable_on Z by A2, FDIFF_2:22;
 for x being Real st x in Z holds
((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies ((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) )
assume A6: x in Z ; ::_thesis: ((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2)))
then A7: ( ln . x <> 0 & ln is_differentiable_in x ) by A2, A4, FDIFF_1:9;
((ln ^) `| Z) . x = diff ((ln ^),x) by A5, A6, FDIFF_1:def_7
.= - ((diff (ln,x)) / ((ln . x) ^2)) by A7, FDIFF_2:15
.= - (((ln `| Z) . x) / ((ln . x) ^2)) by A4, A6, FDIFF_1:def_7
.= - ((1 / x) / ((ln . x) ^2)) by A3, A6, Th19
.= - (1 / (x * ((ln . x) ^2))) by XCMPLX_1:78 ;
hence  ((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) ; ::_thesis: verum
end;
hence  ( ln ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) ) ) by A2, A4, FDIFF_2:22; ::_thesis: verum
end;