:: FDIFF_9 semantic presentation

begin

definition
func sec  ->  PartFunc of REAL,REAL equals :: FDIFF_9:def 1
cos ^ ;
coherence
 cos ^ is PartFunc of REAL,REAL ;
func cosec  ->  PartFunc of REAL,REAL equals :: FDIFF_9:def 2
sin ^ ;
coherence
 sin ^ is PartFunc of REAL,REAL ;
end;

:: deftheorem  defines sec FDIFF_9:def_1_:_
 sec = cos ^ ;

:: deftheorem  defines cosec FDIFF_9:def_2_:_
 cosec = sin ^ ;


theorem Th1: :: FDIFF_9:1
for x being Real st cos . x <> 0 holds
( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
proof
let x be Real; ::_thesis: ( cos . x <> 0 implies ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) )
A1: cos is_differentiable_in x by SIN_COS:63;
assume A2: cos . x <> 0 ; ::_thesis: ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
then  diff ((cos ^),x) = - ((diff (cos,x)) / ((cos . x) ^2)) by A1, FDIFF_2:15
.= - ((- (sin . x)) / ((cos . x) ^2)) by SIN_COS:63
.= (sin . x) / ((cos . x) ^2) ;
hence  ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) by A2, A1, FDIFF_2:15; ::_thesis: verum
end;

theorem Th2: :: FDIFF_9:2
for x being Real st sin . x <> 0 holds
( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
proof
let x be Real; ::_thesis: ( sin . x <> 0 implies ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) )
A1: sin is_differentiable_in x by SIN_COS:64;
assume A2: sin . x <> 0 ; ::_thesis: ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
then  diff ((sin ^),x) = - ((diff (sin,x)) / ((sin . x) ^2)) by A1, FDIFF_2:15
.= - ((cos . x) / ((sin . x) ^2)) by SIN_COS:64 ;
hence  ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) by A2, A1, FDIFF_2:15; ::_thesis: verum
end;

theorem Th3: :: FDIFF_9:3
for x being Real
for n being Nat holds (1 / x) #Z n = 1 / (x #Z n)
proof
let x be Real; ::_thesis: for n being Nat holds (1 / x) #Z n = 1 / (x #Z n)
let n be Nat; ::_thesis: (1 / x) #Z n = 1 / (x #Z n)
(1 / x) #Z n = (1 / x) |^ n by PREPOWER:36
.= 1 / (x |^ n) by PREPOWER:7 ;
hence  (1 / x) #Z n = 1 / (x #Z n) by PREPOWER:36; ::_thesis: verum
end;

theorem :: FDIFF_9:4
for Z being open Subset of REAL st Z c= dom sec holds
( sec is_differentiable_on Z & ( for x being Real st x in Z holds
(sec `| Z) . x = (sin . x) / ((cos . x) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom sec implies ( sec is_differentiable_on Z & ( for x being Real st x in Z holds
(sec `| Z) . x = (sin . x) / ((cos . x) ^2) ) ) )
assume  Z c= dom sec ; ::_thesis: ( sec is_differentiable_on Z & ( for x being Real st x in Z holds
(sec `| Z) . x = (sin . x) / ((cos . x) ^2) ) )
then  for x being Real st x in Z holds
cos . x <> 0 by RFUNCT_1:3;
hence  ( sec is_differentiable_on Z & ( for x being Real st x in Z holds
(sec `| Z) . x = (sin . x) / ((cos . x) ^2) ) ) by FDIFF_4:39; ::_thesis: verum
end;

theorem :: FDIFF_9:5
for Z being open Subset of REAL st Z c= dom cosec holds
( cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(cosec `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom cosec implies ( cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(cosec `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) ) )
assume  Z c= dom cosec ; ::_thesis: ( cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(cosec `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) )
then  for x being Real st x in Z holds
sin . x <> 0 by RFUNCT_1:3;
hence  ( cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(cosec `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) ) by FDIFF_4:40; ::_thesis: verum
end;

theorem Th6: :: FDIFF_9:6
for a, b being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (sec * f) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( sec * f is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * f) `| Z) . x = (a * (sin . ((a * x) + b))) / ((cos . ((a * x) + b)) ^2) ) )
proof
let a, b be Real; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (sec * f) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( sec * f is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * f) `| Z) . x = (a * (sin . ((a * x) + b))) / ((cos . ((a * x) + b)) ^2) ) )
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (sec * f) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( sec * f is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * f) `| Z) . x = (a * (sin . ((a * x) + b))) / ((cos . ((a * x) + b)) ^2) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (sec * f) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) implies ( sec * f is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * f) `| Z) . x = (a * (sin . ((a * x) + b))) / ((cos . ((a * x) + b)) ^2) ) ) )
assume that
A1: Z c= dom (sec * f) and
A2: for x being Real st x in Z holds
f . x = (a * x) + b ; ::_thesis: ( sec * f is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * f) `| Z) . x = (a * (sin . ((a * x) + b))) / ((cos . ((a * x) + b)) ^2) ) )
 dom (sec * f) c= dom f by RELAT_1:25;
then A3: Z c= dom f by A1, XBOOLE_1:1;
then A4: f is_differentiable_on Z by A2, FDIFF_1:23;
A5: for x being Real st x in Z holds
cos . (f . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies cos . (f . x) <> 0 )
assume  x in Z ; ::_thesis: cos . (f . x) <> 0
then  f . x in dom sec by A1, FUNCT_1:11;
hence  cos . (f . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A6: for x being Real st x in Z holds
sec * f is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sec * f is_differentiable_in x )
assume A7: x in Z ; ::_thesis: sec * f is_differentiable_in x
then  cos . (f . x) <> 0 by A5;
then A8: sec is_differentiable_in f . x by Th1;
 f is_differentiable_in x by A4, A7, FDIFF_1:9;
hence  sec * f is_differentiable_in x by A8, FDIFF_2:13; ::_thesis: verum
end;
then A9: sec * f is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sec * f) `| Z) . x = (a * (sin . ((a * x) + b))) / ((cos . ((a * x) + b)) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((sec * f) `| Z) . x = (a * (sin . ((a * x) + b))) / ((cos . ((a * x) + b)) ^2) )
assume A10: x in Z ; ::_thesis: ((sec * f) `| Z) . x = (a * (sin . ((a * x) + b))) / ((cos . ((a * x) + b)) ^2)
then A11: f is_differentiable_in x by A4, FDIFF_1:9;
A12: cos . (f . x) <> 0 by A5, A10;
then  sec is_differentiable_in f . x by Th1;
then  diff ((sec * f),x) = (diff (sec,(f . x))) * (diff (f,x)) by A11, FDIFF_2:13
.= ((sin . (f . x)) / ((cos . (f . x)) ^2)) * (diff (f,x)) by A12, Th1
.= (diff (f,x)) * ((sin . (f . x)) / ((cos . ((a * x) + b)) ^2)) by A2, A10
.= ((f `| Z) . x) * ((sin . (f . x)) / ((cos . ((a * x) + b)) ^2)) by A4, A10, FDIFF_1:def_7
.= a * ((sin . (f . x)) / ((cos . ((a * x) + b)) ^2)) by A2, A3, A10, FDIFF_1:23
.= a * ((sin . ((a * x) + b)) / ((cos . ((a * x) + b)) ^2)) by A2, A10 ;
hence  ((sec * f) `| Z) . x = (a * (sin . ((a * x) + b))) / ((cos . ((a * x) + b)) ^2) by A9, A10, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sec * f is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * f) `| Z) . x = (a * (sin . ((a * x) + b))) / ((cos . ((a * x) + b)) ^2) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum
end;

theorem Th7: :: FDIFF_9:7
for a, b being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (cosec * f) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( cosec * f is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * f) `| Z) . x = - ((a * (cos . ((a * x) + b))) / ((sin . ((a * x) + b)) ^2)) ) )
proof
let a, b be Real; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (cosec * f) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( cosec * f is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * f) `| Z) . x = - ((a * (cos . ((a * x) + b))) / ((sin . ((a * x) + b)) ^2)) ) )
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (cosec * f) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( cosec * f is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * f) `| Z) . x = - ((a * (cos . ((a * x) + b))) / ((sin . ((a * x) + b)) ^2)) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (cosec * f) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) implies ( cosec * f is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * f) `| Z) . x = - ((a * (cos . ((a * x) + b))) / ((sin . ((a * x) + b)) ^2)) ) ) )
assume that
A1: Z c= dom (cosec * f) and
A2: for x being Real st x in Z holds
f . x = (a * x) + b ; ::_thesis: ( cosec * f is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * f) `| Z) . x = - ((a * (cos . ((a * x) + b))) / ((sin . ((a * x) + b)) ^2)) ) )
 dom (cosec * f) c= dom f by RELAT_1:25;
then A3: Z c= dom f by A1, XBOOLE_1:1;
then A4: f is_differentiable_on Z by A2, FDIFF_1:23;
A5: for x being Real st x in Z holds
sin . (f . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . (f . x) <> 0 )
assume  x in Z ; ::_thesis: sin . (f . x) <> 0
then  f . x in dom cosec by A1, FUNCT_1:11;
hence  sin . (f . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A6: for x being Real st x in Z holds
cosec * f is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cosec * f is_differentiable_in x )
assume A7: x in Z ; ::_thesis: cosec * f is_differentiable_in x
then  sin . (f . x) <> 0 by A5;
then A8: cosec is_differentiable_in f . x by Th2;
 f is_differentiable_in x by A4, A7, FDIFF_1:9;
hence  cosec * f is_differentiable_in x by A8, FDIFF_2:13; ::_thesis: verum
end;
then A9: cosec * f is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cosec * f) `| Z) . x = - ((a * (cos . ((a * x) + b))) / ((sin . ((a * x) + b)) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((cosec * f) `| Z) . x = - ((a * (cos . ((a * x) + b))) / ((sin . ((a * x) + b)) ^2)) )
assume A10: x in Z ; ::_thesis: ((cosec * f) `| Z) . x = - ((a * (cos . ((a * x) + b))) / ((sin . ((a * x) + b)) ^2))
then A11: f is_differentiable_in x by A4, FDIFF_1:9;
A12: sin . (f . x) <> 0 by A5, A10;
then  cosec is_differentiable_in f . x by Th2;
then  diff ((cosec * f),x) = (diff (cosec,(f . x))) * (diff (f,x)) by A11, FDIFF_2:13
.= (- ((cos . (f . x)) / ((sin . (f . x)) ^2))) * (diff (f,x)) by A12, Th2
.= (diff (f,x)) * (- ((cos . (f . x)) / ((sin . ((a * x) + b)) ^2))) by A2, A10
.= ((f `| Z) . x) * (- ((cos . (f . x)) / ((sin . ((a * x) + b)) ^2))) by A4, A10, FDIFF_1:def_7
.= a * (- ((cos . (f . x)) / ((sin . ((a * x) + b)) ^2))) by A2, A3, A10, FDIFF_1:23
.= a * (- ((cos . ((a * x) + b)) / ((sin . ((a * x) + b)) ^2))) by A2, A10 ;
hence  ((cosec * f) `| Z) . x = - ((a * (cos . ((a * x) + b))) / ((sin . ((a * x) + b)) ^2)) by A9, A10, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cosec * f is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * f) `| Z) . x = - ((a * (cos . ((a * x) + b))) / ((sin . ((a * x) + b)) ^2)) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:8
for Z being open Subset of REAL st not 0 in Z & Z c= dom (sec * ((id Z) ^)) holds
( sec * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * ((id Z) ^)) `| Z) . x = - ((sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & Z c= dom (sec * ((id Z) ^)) implies ( sec * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * ((id Z) ^)) `| Z) . x = - ((sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2))) ) ) )
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (sec * ((id Z) ^)) ; ::_thesis: ( sec * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * ((id Z) ^)) `| Z) . x = - ((sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2))) ) )
A3: (id Z) ^ is_differentiable_on Z by A1, FDIFF_5:4;
 dom (sec * ((id Z) ^)) c= dom ((id Z) ^) by RELAT_1:25;
then A4: Z c= dom ((id Z) ^) by A2, XBOOLE_1:1;
A5: for x being Real st x in Z holds
cos . (((id Z) ^) . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies cos . (((id Z) ^) . x) <> 0 )
assume  x in Z ; ::_thesis: cos . (((id Z) ^) . x) <> 0
then  ((id Z) ^) . x in dom sec by A2, FUNCT_1:11;
hence  cos . (((id Z) ^) . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A6: for x being Real st x in Z holds
sec * ((id Z) ^) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sec * ((id Z) ^) is_differentiable_in x )
assume A7: x in Z ; ::_thesis: sec * ((id Z) ^) is_differentiable_in x
then  cos . (((id Z) ^) . x) <> 0 by A5;
then A8: sec is_differentiable_in ((id Z) ^) . x by Th1;
 (id Z) ^ is_differentiable_in x by A3, A7, FDIFF_1:9;
hence  sec * ((id Z) ^) is_differentiable_in x by A8, FDIFF_2:13; ::_thesis: verum
end;
then A9: sec * ((id Z) ^) is_differentiable_on Z by A2, FDIFF_1:9;
 for x being Real st x in Z holds
((sec * ((id Z) ^)) `| Z) . x = - ((sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies ((sec * ((id Z) ^)) `| Z) . x = - ((sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2))) )
assume A10: x in Z ; ::_thesis: ((sec * ((id Z) ^)) `| Z) . x = - ((sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)))
then A11: (id Z) ^ is_differentiable_in x by A3, FDIFF_1:9;
A12: cos . (((id Z) ^) . x) <> 0 by A5, A10;
then  sec is_differentiable_in ((id Z) ^) . x by Th1;
then  diff ((sec * ((id Z) ^)),x) = (diff (sec,(((id Z) ^) . x))) * (diff (((id Z) ^),x)) by A11, FDIFF_2:13
.= ((sin . (((id Z) ^) . x)) / ((cos . (((id Z) ^) . x)) ^2)) * (diff (((id Z) ^),x)) by A12, Th1
.= (diff (((id Z) ^),x)) * ((sin . (((id Z) ^) . x)) / ((cos . (((id Z) . x) ")) ^2)) by A4, A10, RFUNCT_1:def_2
.= (diff (((id Z) ^),x)) * ((sin . (((id Z) . x) ")) / ((cos . (((id Z) . x) ")) ^2)) by A4, A10, RFUNCT_1:def_2
.= (diff (((id Z) ^),x)) * ((sin . (((id Z) . x) ")) / ((cos . (1 * (x "))) ^2)) by A10, FUNCT_1:18
.= (diff (((id Z) ^),x)) * ((sin . (1 * (x "))) / ((cos . (1 * (x "))) ^2)) by A10, FUNCT_1:18
.= ((((id Z) ^) `| Z) . x) * ((sin . (1 * (x "))) / ((cos . (1 * (x "))) ^2)) by A3, A10, FDIFF_1:def_7
.= (- (1 / (x ^2))) * ((sin . (1 * (x "))) / ((cos . (1 * (x "))) ^2)) by A1, A10, FDIFF_5:4
.= ((- 1) / (x ^2)) * ((sin . (1 / x)) / ((cos . (1 / x)) ^2))
.= ((- 1) * (sin . (1 / x))) / ((x ^2) * ((cos . (1 / x)) ^2)) by XCMPLX_1:76
.= - ((sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2))) ;
hence  ((sec * ((id Z) ^)) `| Z) . x = - ((sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2))) by A9, A10, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sec * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * ((id Z) ^)) `| Z) . x = - ((sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2))) ) ) by A2, A6, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:9
for Z being open Subset of REAL st not 0 in Z & Z c= dom (cosec * ((id Z) ^)) holds
( cosec * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * ((id Z) ^)) `| Z) . x = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & Z c= dom (cosec * ((id Z) ^)) implies ( cosec * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * ((id Z) ^)) `| Z) . x = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) ) ) )
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (cosec * ((id Z) ^)) ; ::_thesis: ( cosec * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * ((id Z) ^)) `| Z) . x = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) ) )
A3: (id Z) ^ is_differentiable_on Z by A1, FDIFF_5:4;
 dom (cosec * ((id Z) ^)) c= dom ((id Z) ^) by RELAT_1:25;
then A4: Z c= dom ((id Z) ^) by A2, XBOOLE_1:1;
A5: for x being Real st x in Z holds
sin . (((id Z) ^) . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . (((id Z) ^) . x) <> 0 )
assume  x in Z ; ::_thesis: sin . (((id Z) ^) . x) <> 0
then  ((id Z) ^) . x in dom cosec by A2, FUNCT_1:11;
hence  sin . (((id Z) ^) . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A6: for x being Real st x in Z holds
cosec * ((id Z) ^) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cosec * ((id Z) ^) is_differentiable_in x )
assume A7: x in Z ; ::_thesis: cosec * ((id Z) ^) is_differentiable_in x
then  sin . (((id Z) ^) . x) <> 0 by A5;
then A8: cosec is_differentiable_in ((id Z) ^) . x by Th2;
 (id Z) ^ is_differentiable_in x by A3, A7, FDIFF_1:9;
hence  cosec * ((id Z) ^) is_differentiable_in x by A8, FDIFF_2:13; ::_thesis: verum
end;
then A9: cosec * ((id Z) ^) is_differentiable_on Z by A2, FDIFF_1:9;
 for x being Real st x in Z holds
((cosec * ((id Z) ^)) `| Z) . x = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((cosec * ((id Z) ^)) `| Z) . x = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) )
assume A10: x in Z ; ::_thesis: ((cosec * ((id Z) ^)) `| Z) . x = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2))
then A11: (id Z) ^ is_differentiable_in x by A3, FDIFF_1:9;
A12: sin . (((id Z) ^) . x) <> 0 by A5, A10;
then  cosec is_differentiable_in ((id Z) ^) . x by Th2;
then  diff ((cosec * ((id Z) ^)),x) = (diff (cosec,(((id Z) ^) . x))) * (diff (((id Z) ^),x)) by A11, FDIFF_2:13
.= (- ((cos . (((id Z) ^) . x)) / ((sin . (((id Z) ^) . x)) ^2))) * (diff (((id Z) ^),x)) by A12, Th2
.= (diff (((id Z) ^),x)) * (- ((cos . (((id Z) ^) . x)) / ((sin . (((id Z) . x) ")) ^2))) by A4, A10, RFUNCT_1:def_2
.= (diff (((id Z) ^),x)) * (- ((cos . (((id Z) . x) ")) / ((sin . (((id Z) . x) ")) ^2))) by A4, A10, RFUNCT_1:def_2
.= (diff (((id Z) ^),x)) * (- ((cos . (((id Z) . x) ")) / ((sin . (1 * (x "))) ^2))) by A10, FUNCT_1:18
.= (diff (((id Z) ^),x)) * (- ((cos . (1 * (x "))) / ((sin . (1 * (x "))) ^2))) by A10, FUNCT_1:18
.= ((((id Z) ^) `| Z) . x) * (- ((cos . (1 * (x "))) / ((sin . (1 * (x "))) ^2))) by A3, A10, FDIFF_1:def_7
.= (- (1 / (x ^2))) * (- ((cos . (1 * (x "))) / ((sin . (1 * (x "))) ^2))) by A1, A10, FDIFF_5:4
.= ((- 1) / (x ^2)) * ((- (cos . (1 / x))) / ((sin . (1 / x)) ^2))
.= ((- 1) * (- (cos . (1 / x)))) / ((x ^2) * ((sin . (1 / x)) ^2)) by XCMPLX_1:76
.= (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) ;
hence  ((cosec * ((id Z) ^)) `| Z) . x = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) by A9, A10, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cosec * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * ((id Z) ^)) `| Z) . x = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) ) ) by A2, A6, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:10
for c, a, b being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (sec * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = a + (b * x) ) holds
( sec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * (f1 + (c (#) f2))) `| Z) . x = ((b + ((2 * c) * x)) * (sin . ((a + (b * x)) + (c * (x ^2))))) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) ) )
proof
let c, a, b be Real; ::_thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (sec * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = a + (b * x) ) holds
( sec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * (f1 + (c (#) f2))) `| Z) . x = ((b + ((2 * c) * x)) * (sin . ((a + (b * x)) + (c * (x ^2))))) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) ) )
let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (sec * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = a + (b * x) ) holds
( sec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * (f1 + (c (#) f2))) `| Z) . x = ((b + ((2 * c) * x)) * (sin . ((a + (b * x)) + (c * (x ^2))))) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) ) )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (sec * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = a + (b * x) ) implies ( sec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * (f1 + (c (#) f2))) `| Z) . x = ((b + ((2 * c) * x)) * (sin . ((a + (b * x)) + (c * (x ^2))))) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) ) ) )
assume that
A1: Z c= dom (sec * (f1 + (c (#) f2))) and
A2: f2 = #Z 2 and
A3: for x being Real st x in Z holds
f1 . x = a + (b * x) ; ::_thesis: ( sec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * (f1 + (c (#) f2))) `| Z) . x = ((b + ((2 * c) * x)) * (sin . ((a + (b * x)) + (c * (x ^2))))) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) ) )
 dom (sec * (f1 + (c (#) f2))) c= dom (f1 + (c (#) f2)) by RELAT_1:25;
then A4: Z c= dom (f1 + (c (#) f2)) by A1, XBOOLE_1:1;
then A5: f1 + (c (#) f2) is_differentiable_on Z by A2, A3, FDIFF_4:12;
 Z c= (dom f1) /\ (dom (c (#) f2)) by A4, VALUED_1:def_1;
then A6: Z c= dom (c (#) f2) by XBOOLE_1:18;
A7: for x being Real st x in Z holds
cos . ((f1 + (c (#) f2)) . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies cos . ((f1 + (c (#) f2)) . x) <> 0 )
assume  x in Z ; ::_thesis: cos . ((f1 + (c (#) f2)) . x) <> 0
then  (f1 + (c (#) f2)) . x in dom sec by A1, FUNCT_1:11;
hence  cos . ((f1 + (c (#) f2)) . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A8: for x being Real st x in Z holds
sec * (f1 + (c (#) f2)) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sec * (f1 + (c (#) f2)) is_differentiable_in x )
assume A9: x in Z ; ::_thesis: sec * (f1 + (c (#) f2)) is_differentiable_in x
then  cos . ((f1 + (c (#) f2)) . x) <> 0 by A7;
then A10: sec is_differentiable_in (f1 + (c (#) f2)) . x by Th1;
 f1 + (c (#) f2) is_differentiable_in x by A5, A9, FDIFF_1:9;
hence  sec * (f1 + (c (#) f2)) is_differentiable_in x by A10, FDIFF_2:13; ::_thesis: verum
end;
then A11: sec * (f1 + (c (#) f2)) is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sec * (f1 + (c (#) f2))) `| Z) . x = ((b + ((2 * c) * x)) * (sin . ((a + (b * x)) + (c * (x ^2))))) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((sec * (f1 + (c (#) f2))) `| Z) . x = ((b + ((2 * c) * x)) * (sin . ((a + (b * x)) + (c * (x ^2))))) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) )
assume A12: x in Z ; ::_thesis: ((sec * (f1 + (c (#) f2))) `| Z) . x = ((b + ((2 * c) * x)) * (sin . ((a + (b * x)) + (c * (x ^2))))) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2)
then A13: (f1 + (c (#) f2)) . x = (f1 . x) + ((c (#) f2) . x) by A4, VALUED_1:def_1
.= (f1 . x) + (c * (f2 . x)) by A6, A12, VALUED_1:def_5
.= (a + (b * x)) + (c * (f2 . x)) by A3, A12
.= (a + (b * x)) + (c * (x #Z 2)) by A2, TAYLOR_1:def_1
.= (a + (b * x)) + (c * (x |^ 2)) by PREPOWER:36
.= (a + (b * x)) + (c * (x ^2)) by NEWTON:81 ;
A14: f1 + (c (#) f2) is_differentiable_in x by A5, A12, FDIFF_1:9;
A15: cos . ((f1 + (c (#) f2)) . x) <> 0 by A7, A12;
then  sec is_differentiable_in (f1 + (c (#) f2)) . x by Th1;
then  diff ((sec * (f1 + (c (#) f2))),x) = (diff (sec,((f1 + (c (#) f2)) . x))) * (diff ((f1 + (c (#) f2)),x)) by A14, FDIFF_2:13
.= ((sin . ((f1 + (c (#) f2)) . x)) / ((cos . ((f1 + (c (#) f2)) . x)) ^2)) * (diff ((f1 + (c (#) f2)),x)) by A15, Th1
.= (((f1 + (c (#) f2)) `| Z) . x) * ((sin . ((a + (b * x)) + (c * (x ^2)))) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2)) by A5, A12, A13, FDIFF_1:def_7
.= (b + ((2 * c) * x)) * ((sin . ((a + (b * x)) + (c * (x ^2)))) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2)) by A2, A3, A4, A12, FDIFF_4:12 ;
hence  ((sec * (f1 + (c (#) f2))) `| Z) . x = ((b + ((2 * c) * x)) * (sin . ((a + (b * x)) + (c * (x ^2))))) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) by A11, A12, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * (f1 + (c (#) f2))) `| Z) . x = ((b + ((2 * c) * x)) * (sin . ((a + (b * x)) + (c * (x ^2))))) / ((cos . ((a + (b * x)) + (c * (x ^2)))) ^2) ) ) by A1, A8, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:11
for c, a, b being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (cosec * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = a + (b * x) ) holds
( cosec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) )
proof
let c, a, b be Real; ::_thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (cosec * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = a + (b * x) ) holds
( cosec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) )
let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (cosec * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = a + (b * x) ) holds
( cosec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (cosec * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = a + (b * x) ) implies ( cosec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) ) )
assume that
A1: Z c= dom (cosec * (f1 + (c (#) f2))) and
A2: f2 = #Z 2 and
A3: for x being Real st x in Z holds
f1 . x = a + (b * x) ; ::_thesis: ( cosec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) )
 dom (cosec * (f1 + (c (#) f2))) c= dom (f1 + (c (#) f2)) by RELAT_1:25;
then A4: Z c= dom (f1 + (c (#) f2)) by A1, XBOOLE_1:1;
then A5: f1 + (c (#) f2) is_differentiable_on Z by A2, A3, FDIFF_4:12;
 Z c= (dom f1) /\ (dom (c (#) f2)) by A4, VALUED_1:def_1;
then A6: Z c= dom (c (#) f2) by XBOOLE_1:18;
A7: for x being Real st x in Z holds
sin . ((f1 + (c (#) f2)) . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . ((f1 + (c (#) f2)) . x) <> 0 )
assume  x in Z ; ::_thesis: sin . ((f1 + (c (#) f2)) . x) <> 0
then  (f1 + (c (#) f2)) . x in dom cosec by A1, FUNCT_1:11;
hence  sin . ((f1 + (c (#) f2)) . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A8: for x being Real st x in Z holds
cosec * (f1 + (c (#) f2)) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cosec * (f1 + (c (#) f2)) is_differentiable_in x )
assume A9: x in Z ; ::_thesis: cosec * (f1 + (c (#) f2)) is_differentiable_in x
then  sin . ((f1 + (c (#) f2)) . x) <> 0 by A7;
then A10: cosec is_differentiable_in (f1 + (c (#) f2)) . x by Th2;
 f1 + (c (#) f2) is_differentiable_in x by A5, A9, FDIFF_1:9;
hence  cosec * (f1 + (c (#) f2)) is_differentiable_in x by A10, FDIFF_2:13; ::_thesis: verum
end;
then A11: cosec * (f1 + (c (#) f2)) is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) )
assume A12: x in Z ; ::_thesis: ((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2))
then A13: (f1 + (c (#) f2)) . x = (f1 . x) + ((c (#) f2) . x) by A4, VALUED_1:def_1
.= (f1 . x) + (c * (f2 . x)) by A6, A12, VALUED_1:def_5
.= (a + (b * x)) + (c * (f2 . x)) by A3, A12
.= (a + (b * x)) + (c * (x #Z 2)) by A2, TAYLOR_1:def_1
.= (a + (b * x)) + (c * (x |^ 2)) by PREPOWER:36
.= (a + (b * x)) + (c * (x ^2)) by NEWTON:81 ;
A14: f1 + (c (#) f2) is_differentiable_in x by A5, A12, FDIFF_1:9;
A15: sin . ((f1 + (c (#) f2)) . x) <> 0 by A7, A12;
then  cosec is_differentiable_in (f1 + (c (#) f2)) . x by Th2;
then  diff ((cosec * (f1 + (c (#) f2))),x) = (diff (cosec,((f1 + (c (#) f2)) . x))) * (diff ((f1 + (c (#) f2)),x)) by A14, FDIFF_2:13
.= (- ((cos . ((f1 + (c (#) f2)) . x)) / ((sin . ((f1 + (c (#) f2)) . x)) ^2))) * (diff ((f1 + (c (#) f2)),x)) by A15, Th2
.= (((f1 + (c (#) f2)) `| Z) . x) * (- ((cos . ((a + (b * x)) + (c * (x ^2)))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2))) by A5, A12, A13, FDIFF_1:def_7
.= (b + ((2 * c) * x)) * (- ((cos . ((a + (b * x)) + (c * (x ^2)))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2))) by A2, A3, A4, A12, FDIFF_4:12 ;
hence  ((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) by A11, A12, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cosec * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * (f1 + (c (#) f2))) `| Z) . x = - (((b + ((2 * c) * x)) * (cos . ((a + (b * x)) + (c * (x ^2))))) / ((sin . ((a + (b * x)) + (c * (x ^2)))) ^2)) ) ) by A1, A8, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:12
for Z being open Subset of REAL st Z c= dom (sec * exp_R) holds
( sec * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * exp_R) `| Z) . x = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sec * exp_R) implies ( sec * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * exp_R) `| Z) . x = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) ) ) )
assume A1: Z c= dom (sec * exp_R) ; ::_thesis: ( sec * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * exp_R) `| Z) . x = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) ) )
A2: for x being Real st x in Z holds
cos . (exp_R . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies cos . (exp_R . x) <> 0 )
assume  x in Z ; ::_thesis: cos . (exp_R . x) <> 0
then  exp_R . x in dom sec by A1, FUNCT_1:11;
hence  cos . (exp_R . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A3: for x being Real st x in Z holds
sec * exp_R is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sec * exp_R is_differentiable_in x )
assume  x in Z ; ::_thesis: sec * exp_R is_differentiable_in x
then  cos . (exp_R . x) <> 0 by A2;
then  ( exp_R is_differentiable_in x & sec is_differentiable_in exp_R . x ) by Th1, SIN_COS:65;
hence  sec * exp_R is_differentiable_in x by FDIFF_2:13; ::_thesis: verum
end;
then A4: sec * exp_R is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sec * exp_R) `| Z) . x = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((sec * exp_R) `| Z) . x = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) )
assume A5: x in Z ; ::_thesis: ((sec * exp_R) `| Z) . x = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2)
then A6: cos . (exp_R . x) <> 0 by A2;
then  ( exp_R is_differentiable_in x & sec is_differentiable_in exp_R . x ) by Th1, SIN_COS:65;
then  diff ((sec * exp_R),x) = (diff (sec,(exp_R . x))) * (diff (exp_R,x)) by FDIFF_2:13
.= ((sin . (exp_R . x)) / ((cos . (exp_R . x)) ^2)) * (diff (exp_R,x)) by A6, Th1
.= (exp_R . x) * ((sin . (exp_R . x)) / ((cos . (exp_R . x)) ^2)) by SIN_COS:65 ;
hence  ((sec * exp_R) `| Z) . x = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) by A4, A5, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sec * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * exp_R) `| Z) . x = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:13
for Z being open Subset of REAL st Z c= dom (cosec * exp_R) holds
( cosec * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * exp_R) `| Z) . x = - (((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cosec * exp_R) implies ( cosec * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * exp_R) `| Z) . x = - (((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2)) ) ) )
assume A1: Z c= dom (cosec * exp_R) ; ::_thesis: ( cosec * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * exp_R) `| Z) . x = - (((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2)) ) )
A2: for x being Real st x in Z holds
sin . (exp_R . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . (exp_R . x) <> 0 )
assume  x in Z ; ::_thesis: sin . (exp_R . x) <> 0
then  exp_R . x in dom cosec by A1, FUNCT_1:11;
hence  sin . (exp_R . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A3: for x being Real st x in Z holds
cosec * exp_R is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cosec * exp_R is_differentiable_in x )
assume  x in Z ; ::_thesis: cosec * exp_R is_differentiable_in x
then  sin . (exp_R . x) <> 0 by A2;
then  ( exp_R is_differentiable_in x & cosec is_differentiable_in exp_R . x ) by Th2, SIN_COS:65;
hence  cosec * exp_R is_differentiable_in x by FDIFF_2:13; ::_thesis: verum
end;
then A4: cosec * exp_R is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cosec * exp_R) `| Z) . x = - (((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((cosec * exp_R) `| Z) . x = - (((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2)) )
assume A5: x in Z ; ::_thesis: ((cosec * exp_R) `| Z) . x = - (((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2))
then A6: sin . (exp_R . x) <> 0 by A2;
then  ( exp_R is_differentiable_in x & cosec is_differentiable_in exp_R . x ) by Th2, SIN_COS:65;
then  diff ((cosec * exp_R),x) = (diff (cosec,(exp_R . x))) * (diff (exp_R,x)) by FDIFF_2:13
.= (- ((cos . (exp_R . x)) / ((sin . (exp_R . x)) ^2))) * (diff (exp_R,x)) by A6, Th2
.= (exp_R . x) * (- ((cos . (exp_R . x)) / ((sin . (exp_R . x)) ^2))) by SIN_COS:65 ;
hence  ((cosec * exp_R) `| Z) . x = - (((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2)) by A4, A5, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cosec * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * exp_R) `| Z) . x = - (((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2)) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum
end;

Lm1:  right_open_halfline 0 =  {  g where g is Real : 0 < g  }
by XXREAL_1:230;

theorem :: FDIFF_9:14
for Z being open Subset of REAL st Z c= dom (sec * ln) holds
( sec * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * ln) `| Z) . x = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sec * ln) implies ( sec * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * ln) `| Z) . x = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) ) ) )
assume A1: Z c= dom (sec * ln) ; ::_thesis: ( sec * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * ln) `| Z) . x = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) ) )
 dom (sec * ln) c= dom ln by RELAT_1:25;
then A2: Z c= dom ln by A1, XBOOLE_1:1;
A3: for x being Real st x in Z holds
x > 0
proof
let x be Real; ::_thesis: ( x in Z implies x > 0 )
assume  x in Z ; ::_thesis: x > 0
then  x in right_open_halfline 0 by A2, TAYLOR_1:18;
then  ex g being Real st
( x = g & 0 < g ) by Lm1;
hence  x > 0 ; ::_thesis: verum
end;
A4: for x being Real st x in Z holds
diff (ln,x) = 1 / x
proof
let x be Real; ::_thesis: ( x in Z implies diff (ln,x) = 1 / x )
assume  x in Z ; ::_thesis: diff (ln,x) = 1 / x
then  x > 0 by A3;
then  x in right_open_halfline 0 by Lm1;
hence  diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum
end;
A5: for x being Real st x in Z holds
cos . (ln . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies cos . (ln . x) <> 0 )
assume  x in Z ; ::_thesis: cos . (ln . x) <> 0
then  ln . x in dom sec by A1, FUNCT_1:11;
hence  cos . (ln . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A6: for x being Real st x in Z holds
sec * ln is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sec * ln is_differentiable_in x )
assume A7: x in Z ; ::_thesis: sec * ln is_differentiable_in x
then  cos . (ln . x) <> 0 by A5;
then A8: sec is_differentiable_in ln . x by Th1;
 ln is_differentiable_in x by A3, A7, TAYLOR_1:18;
hence  sec * ln is_differentiable_in x by A8, FDIFF_2:13; ::_thesis: verum
end;
then A9: sec * ln is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sec * ln) `| Z) . x = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((sec * ln) `| Z) . x = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) )
assume A10: x in Z ; ::_thesis: ((sec * ln) `| Z) . x = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2))
then A11: ln is_differentiable_in x by A3, TAYLOR_1:18;
A12: cos . (ln . x) <> 0 by A5, A10;
then  sec is_differentiable_in ln . x by Th1;
then  diff ((sec * ln),x) = (diff (sec,(ln . x))) * (diff (ln,x)) by A11, FDIFF_2:13
.= ((sin . (ln . x)) / ((cos . (ln . x)) ^2)) * (diff (ln,x)) by A12, Th1
.= (1 / x) * ((sin . (ln . x)) / ((cos . (ln . x)) ^2)) by A4, A10
.= (1 * (sin . (ln . x))) / (x * ((cos . (ln . x)) ^2)) by XCMPLX_1:76 ;
hence  ((sec * ln) `| Z) . x = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) by A9, A10, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sec * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * ln) `| Z) . x = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:15
for Z being open Subset of REAL st Z c= dom (cosec * ln) holds
( cosec * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cosec * ln) implies ( cosec * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2))) ) ) )
assume A1: Z c= dom (cosec * ln) ; ::_thesis: ( cosec * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2))) ) )
 dom (cosec * ln) c= dom ln by RELAT_1:25;
then A2: Z c= dom ln by A1, XBOOLE_1:1;
A3: for x being Real st x in Z holds
x > 0
proof
let x be Real; ::_thesis: ( x in Z implies x > 0 )
assume  x in Z ; ::_thesis: x > 0
then  x in right_open_halfline 0 by A2, TAYLOR_1:18;
then  ex g being Real st
( x = g & 0 < g ) by Lm1;
hence  x > 0 ; ::_thesis: verum
end;
A4: for x being Real st x in Z holds
diff (ln,x) = 1 / x
proof
let x be Real; ::_thesis: ( x in Z implies diff (ln,x) = 1 / x )
assume  x in Z ; ::_thesis: diff (ln,x) = 1 / x
then  x > 0 by A3;
then  x in right_open_halfline 0 by Lm1;
hence  diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum
end;
A5: for x being Real st x in Z holds
sin . (ln . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . (ln . x) <> 0 )
assume  x in Z ; ::_thesis: sin . (ln . x) <> 0
then  ln . x in dom cosec by A1, FUNCT_1:11;
hence  sin . (ln . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A6: for x being Real st x in Z holds
cosec * ln is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cosec * ln is_differentiable_in x )
assume A7: x in Z ; ::_thesis: cosec * ln is_differentiable_in x
then  sin . (ln . x) <> 0 by A5;
then A8: cosec is_differentiable_in ln . x by Th2;
 ln is_differentiable_in x by A3, A7, TAYLOR_1:18;
hence  cosec * ln is_differentiable_in x by A8, FDIFF_2:13; ::_thesis: verum
end;
then A9: cosec * ln is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies ((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2))) )
assume A10: x in Z ; ::_thesis: ((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)))
then A11: ln is_differentiable_in x by A3, TAYLOR_1:18;
A12: sin . (ln . x) <> 0 by A5, A10;
then  cosec is_differentiable_in ln . x by Th2;
then  diff ((cosec * ln),x) = (diff (cosec,(ln . x))) * (diff (ln,x)) by A11, FDIFF_2:13
.= (- ((cos . (ln . x)) / ((sin . (ln . x)) ^2))) * (diff (ln,x)) by A12, Th2
.= (1 / x) * ((- (cos . (ln . x))) / ((sin . (ln . x)) ^2)) by A4, A10
.= (1 * (- (cos . (ln . x)))) / (x * ((sin . (ln . x)) ^2)) by XCMPLX_1:76 ;
hence  ((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2))) by A9, A10, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cosec * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2))) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:16
for Z being open Subset of REAL st Z c= dom (exp_R * sec) holds
( exp_R * sec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * sec) `| Z) . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * sec) implies ( exp_R * sec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * sec) `| Z) . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) ) ) )
assume A1: Z c= dom (exp_R * sec) ; ::_thesis: ( exp_R * sec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * sec) `| Z) . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) ) )
A2: for x being Real st x in Z holds
cos . x <> 0
proof
let x be Real; ::_thesis: ( x in Z implies cos . x <> 0 )
assume  x in Z ; ::_thesis: cos . x <> 0
then  x in dom sec by A1, FUNCT_1:11;
hence  cos . x <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A3: for x being Real st x in Z holds
exp_R * sec is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies exp_R * sec is_differentiable_in x )
assume  x in Z ; ::_thesis: exp_R * sec is_differentiable_in x
then  cos . x <> 0 by A2;
then A4: sec is_differentiable_in x by Th1;
 exp_R is_differentiable_in sec . x by SIN_COS:65;
hence  exp_R * sec is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum
end;
then A5: exp_R * sec is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((exp_R * sec) `| Z) . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((exp_R * sec) `| Z) . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) )
A6: exp_R is_differentiable_in sec . x by SIN_COS:65;
assume A7: x in Z ; ::_thesis: ((exp_R * sec) `| Z) . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2)
then A8: cos . x <> 0 by A2;
then  sec is_differentiable_in x by Th1;
then  diff ((exp_R * sec),x) = (diff (exp_R,(sec . x))) * (diff (sec,x)) by A6, FDIFF_2:13
.= (diff (exp_R,(sec . x))) * ((sin . x) / ((cos . x) ^2)) by A8, Th1
.= (exp_R . (sec . x)) * ((sin . x) / ((cos . x) ^2)) by SIN_COS:65 ;
hence  ((exp_R * sec) `| Z) . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) by A5, A7, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( exp_R * sec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * sec) `| Z) . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:17
for Z being open Subset of REAL st Z c= dom (exp_R * cosec) holds
( exp_R * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * cosec) `| Z) . x = - (((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * cosec) implies ( exp_R * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * cosec) `| Z) . x = - (((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) ) ) )
assume A1: Z c= dom (exp_R * cosec) ; ::_thesis: ( exp_R * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * cosec) `| Z) . x = - (((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) ) )
A2: for x being Real st x in Z holds
sin . x <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . x <> 0 )
assume  x in Z ; ::_thesis: sin . x <> 0
then  x in dom cosec by A1, FUNCT_1:11;
hence  sin . x <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A3: for x being Real st x in Z holds
exp_R * cosec is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies exp_R * cosec is_differentiable_in x )
assume  x in Z ; ::_thesis: exp_R * cosec is_differentiable_in x
then  sin . x <> 0 by A2;
then A4: cosec is_differentiable_in x by Th2;
 exp_R is_differentiable_in cosec . x by SIN_COS:65;
hence  exp_R * cosec is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum
end;
then A5: exp_R * cosec is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((exp_R * cosec) `| Z) . x = - (((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((exp_R * cosec) `| Z) . x = - (((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) )
A6: exp_R is_differentiable_in cosec . x by SIN_COS:65;
assume A7: x in Z ; ::_thesis: ((exp_R * cosec) `| Z) . x = - (((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2))
then A8: sin . x <> 0 by A2;
then  cosec is_differentiable_in x by Th2;
then  diff ((exp_R * cosec),x) = (diff (exp_R,(cosec . x))) * (diff (cosec,x)) by A6, FDIFF_2:13
.= (diff (exp_R,(cosec . x))) * (- ((cos . x) / ((sin . x) ^2))) by A8, Th2
.= (exp_R . (cosec . x)) * (- ((cos . x) / ((sin . x) ^2))) by SIN_COS:65 ;
hence  ((exp_R * cosec) `| Z) . x = - (((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) by A5, A7, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( exp_R * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * cosec) `| Z) . x = - (((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:18
for Z being open Subset of REAL st Z c= dom (ln * sec) holds
( ln * sec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * sec) `| Z) . x = (sin . x) / (cos . x) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln * sec) implies ( ln * sec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * sec) `| Z) . x = (sin . x) / (cos . x) ) ) )
assume A1: Z c= dom (ln * sec) ; ::_thesis: ( ln * sec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * sec) `| Z) . x = (sin . x) / (cos . x) ) )
A2: for x being Real st x in Z holds
sec . x > 0
proof
let x be Real; ::_thesis: ( x in Z implies sec . x > 0 )
assume  x in Z ; ::_thesis: sec . x > 0
then  sec . x in right_open_halfline 0 by A1, FUNCT_1:11, TAYLOR_1:18;
then  ex g being Real st
( sec . x = g & 0 < g ) by Lm1;
hence  sec . x > 0 ; ::_thesis: verum
end;
 dom (ln * sec) c= dom sec by RELAT_1:25;
then A3: Z c= dom sec by A1, XBOOLE_1:1;
A4: for x being Real st x in Z holds
cos . x <> 0
proof
let x be Real; ::_thesis: ( x in Z implies cos . x <> 0 )
assume  x in Z ; ::_thesis: cos . x <> 0
then  x in dom sec by A1, FUNCT_1:11;
hence  cos . x <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A5: for x being Real st x in Z holds
sec is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sec is_differentiable_in x )
assume  x in Z ; ::_thesis: sec is_differentiable_in x
then  cos . x <> 0 by A4;
hence  sec is_differentiable_in x by Th1; ::_thesis: verum
end;
A6: for x being Real st x in Z holds
ln * sec is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies ln * sec is_differentiable_in x )
assume  x in Z ; ::_thesis: ln * sec is_differentiable_in x
then  ( sec is_differentiable_in x & sec . x > 0 ) by A2, A5;
hence  ln * sec is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum
end;
then A7: ln * sec is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((ln * sec) `| Z) . x = (sin . x) / (cos . x)
proof
let x be Real; ::_thesis: ( x in Z implies ((ln * sec) `| Z) . x = (sin . x) / (cos . x) )
assume A8: x in Z ; ::_thesis: ((ln * sec) `| Z) . x = (sin . x) / (cos . x)
then A9: cos . x <> 0 by A4;
 ( sec is_differentiable_in x & sec . x > 0 ) by A2, A5, A8;
then  diff ((ln * sec),x) = (diff (sec,x)) / (sec . x) by TAYLOR_1:20
.= ((sin . x) / ((cos . x) ^2)) / (sec . x) by A9, Th1
.= ((sin . x) / ((cos . x) ^2)) / ((cos . x) ") by A3, A8, RFUNCT_1:def_2
.= ((sin . x) * (cos . x)) / ((cos . x) * (cos . x))
.= (sin . x) / (cos . x) by A4, A8, XCMPLX_1:91 ;
hence  ((ln * sec) `| Z) . x = (sin . x) / (cos . x) by A7, A8, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( ln * sec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * sec) `| Z) . x = (sin . x) / (cos . x) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:19
for Z being open Subset of REAL st Z c= dom (ln * cosec) holds
( ln * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * cosec) `| Z) . x = - ((cos . x) / (sin . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln * cosec) implies ( ln * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * cosec) `| Z) . x = - ((cos . x) / (sin . x)) ) ) )
assume A1: Z c= dom (ln * cosec) ; ::_thesis: ( ln * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * cosec) `| Z) . x = - ((cos . x) / (sin . x)) ) )
A2: for x being Real st x in Z holds
cosec . x > 0
proof
let x be Real; ::_thesis: ( x in Z implies cosec . x > 0 )
assume  x in Z ; ::_thesis: cosec . x > 0
then  cosec . x in right_open_halfline 0 by A1, FUNCT_1:11, TAYLOR_1:18;
then  ex g being Real st
( cosec . x = g & 0 < g ) by Lm1;
hence  cosec . x > 0 ; ::_thesis: verum
end;
 dom (ln * cosec) c= dom cosec by RELAT_1:25;
then A3: Z c= dom cosec by A1, XBOOLE_1:1;
A4: for x being Real st x in Z holds
sin . x <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . x <> 0 )
assume  x in Z ; ::_thesis: sin . x <> 0
then  x in dom cosec by A1, FUNCT_1:11;
hence  sin . x <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A5: for x being Real st x in Z holds
cosec is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cosec is_differentiable_in x )
assume  x in Z ; ::_thesis: cosec is_differentiable_in x
then  sin . x <> 0 by A4;
hence  cosec is_differentiable_in x by Th2; ::_thesis: verum
end;
A6: for x being Real st x in Z holds
ln * cosec is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies ln * cosec is_differentiable_in x )
assume  x in Z ; ::_thesis: ln * cosec is_differentiable_in x
then  ( cosec is_differentiable_in x & cosec . x > 0 ) by A2, A5;
hence  ln * cosec is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum
end;
then A7: ln * cosec is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((ln * cosec) `| Z) . x = - ((cos . x) / (sin . x))
proof
let x be Real; ::_thesis: ( x in Z implies ((ln * cosec) `| Z) . x = - ((cos . x) / (sin . x)) )
assume A8: x in Z ; ::_thesis: ((ln * cosec) `| Z) . x = - ((cos . x) / (sin . x))
then A9: sin . x <> 0 by A4;
 ( cosec is_differentiable_in x & cosec . x > 0 ) by A2, A5, A8;
then  diff ((ln * cosec),x) = (diff (cosec,x)) / (cosec . x) by TAYLOR_1:20
.= (- ((cos . x) / ((sin . x) ^2))) / (cosec . x) by A9, Th2
.= (- ((cos . x) / ((sin . x) ^2))) / ((sin . x) ") by A3, A8, RFUNCT_1:def_2
.= ((- (cos . x)) * (sin . x)) / ((sin . x) * (sin . x))
.= (- (cos . x)) / (sin . x) by A4, A8, XCMPLX_1:91 ;
hence  ((ln * cosec) `| Z) . x = - ((cos . x) / (sin . x)) by A7, A8, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( ln * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * cosec) `| Z) . x = - ((cos . x) / (sin . x)) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:20
for n being Nat
for Z being open Subset of REAL st Z c= dom ((#Z n) * sec) & 1 <= n holds
( (#Z n) * sec is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * sec) `| Z) . x = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) )
proof
let n be Nat; ::_thesis: for Z being open Subset of REAL st Z c= dom ((#Z n) * sec) & 1 <= n holds
( (#Z n) * sec is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * sec) `| Z) . x = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) )
let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((#Z n) * sec) & 1 <= n implies ( (#Z n) * sec is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * sec) `| Z) . x = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) ) )
assume that
A1: Z c= dom ((#Z n) * sec) and
A2: 1 <= n ; ::_thesis: ( (#Z n) * sec is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * sec) `| Z) . x = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) )
 dom ((#Z n) * sec) c= dom sec by RELAT_1:25;
then A3: Z c= dom sec by A1, XBOOLE_1:1;
A4: for x being Real st x in Z holds
cos . x <> 0
proof
let x be Real; ::_thesis: ( x in Z implies cos . x <> 0 )
assume  x in Z ; ::_thesis: cos . x <> 0
then  x in dom sec by A1, FUNCT_1:11;
hence  cos . x <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A5: for x being Real st x in Z holds
(#Z n) * sec is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies (#Z n) * sec is_differentiable_in x )
assume  x in Z ; ::_thesis: (#Z n) * sec is_differentiable_in x
then  cos . x <> 0 by A4;
then  sec is_differentiable_in x by Th1;
hence  (#Z n) * sec is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum
end;
then A6: (#Z n) * sec is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
(((#Z n) * sec) `| Z) . x = (n * (sin . x)) / ((cos . x) #Z (n + 1))
proof
set m = n - 1;
let x be Real; ::_thesis: ( x in Z implies (((#Z n) * sec) `| Z) . x = (n * (sin . x)) / ((cos . x) #Z (n + 1)) )
A7: ex m being Nat st n = m + 1 by A2, NAT_1:6;
assume A8: x in Z ; ::_thesis: (((#Z n) * sec) `| Z) . x = (n * (sin . x)) / ((cos . x) #Z (n + 1))
then A9: cos . x <> 0 by A4;
then A10: sec is_differentiable_in x by Th1;
(((#Z n) * sec) `| Z) . x = diff (((#Z n) * sec),x) by A6, A8, FDIFF_1:def_7
.= (n * ((sec . x) #Z (n - 1))) * (diff (sec,x)) by A10, TAYLOR_1:3
.= (n * ((sec . x) #Z (n - 1))) * ((sin . x) / ((cos . x) ^2)) by A9, Th1
.= (n * ((1 / (cos . x)) #Z (n - 1))) * ((sin . x) / ((cos . x) ^2)) by A3, A8, RFUNCT_1:def_2
.= (n * (1 / ((cos . x) #Z (n - 1)))) * ((sin . x) / ((cos . x) ^2)) by A7, Th3
.= (n / ((cos . x) #Z (n - 1))) * ((sin . x) / ((cos . x) ^2))
.= (n * (sin . x)) / (((cos . x) #Z (n - 1)) * ((cos . x) ^2)) by XCMPLX_1:76
.= (n * (sin . x)) / (((cos . x) #Z (n - 1)) * ((cos . x) #Z 2)) by FDIFF_7:1
.= (n * (sin . x)) / ((cos . x) #Z ((n - 1) + 2)) by A4, A8, PREPOWER:44
.= (n * (sin . x)) / ((cos . x) #Z (n + 1)) ;
hence  (((#Z n) * sec) `| Z) . x = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ; ::_thesis: verum
end;
hence  ( (#Z n) * sec is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * sec) `| Z) . x = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) ) by A1, A5, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:21
for n being Nat
for Z being open Subset of REAL st Z c= dom ((#Z n) * cosec) & 1 <= n holds
( (#Z n) * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * cosec) `| Z) . x = - ((n * (cos . x)) / ((sin . x) #Z (n + 1))) ) )
proof
let n be Nat; ::_thesis: for Z being open Subset of REAL st Z c= dom ((#Z n) * cosec) & 1 <= n holds
( (#Z n) * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * cosec) `| Z) . x = - ((n * (cos . x)) / ((sin . x) #Z (n + 1))) ) )
let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((#Z n) * cosec) & 1 <= n implies ( (#Z n) * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * cosec) `| Z) . x = - ((n * (cos . x)) / ((sin . x) #Z (n + 1))) ) ) )
assume that
A1: Z c= dom ((#Z n) * cosec) and
A2: 1 <= n ; ::_thesis: ( (#Z n) * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * cosec) `| Z) . x = - ((n * (cos . x)) / ((sin . x) #Z (n + 1))) ) )
 dom ((#Z n) * cosec) c= dom cosec by RELAT_1:25;
then A3: Z c= dom cosec by A1, XBOOLE_1:1;
A4: for x being Real st x in Z holds
sin . x <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . x <> 0 )
assume  x in Z ; ::_thesis: sin . x <> 0
then  x in dom cosec by A1, FUNCT_1:11;
hence  sin . x <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A5: for x being Real st x in Z holds
(#Z n) * cosec is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies (#Z n) * cosec is_differentiable_in x )
assume  x in Z ; ::_thesis: (#Z n) * cosec is_differentiable_in x
then  sin . x <> 0 by A4;
then  cosec is_differentiable_in x by Th2;
hence  (#Z n) * cosec is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum
end;
then A6: (#Z n) * cosec is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
(((#Z n) * cosec) `| Z) . x = - ((n * (cos . x)) / ((sin . x) #Z (n + 1)))
proof
set m = n - 1;
let x be Real; ::_thesis: ( x in Z implies (((#Z n) * cosec) `| Z) . x = - ((n * (cos . x)) / ((sin . x) #Z (n + 1))) )
A7: ex m being Nat st n = m + 1 by A2, NAT_1:6;
assume A8: x in Z ; ::_thesis: (((#Z n) * cosec) `| Z) . x = - ((n * (cos . x)) / ((sin . x) #Z (n + 1)))
then A9: sin . x <> 0 by A4;
then A10: cosec is_differentiable_in x by Th2;
(((#Z n) * cosec) `| Z) . x = diff (((#Z n) * cosec),x) by A6, A8, FDIFF_1:def_7
.= (n * ((cosec . x) #Z (n - 1))) * (diff (cosec,x)) by A10, TAYLOR_1:3
.= (n * ((cosec . x) #Z (n - 1))) * (- ((cos . x) / ((sin . x) ^2))) by A9, Th2
.= (n * ((1 / (sin . x)) #Z (n - 1))) * (- ((cos . x) / ((sin . x) ^2))) by A3, A8, RFUNCT_1:def_2
.= (n * (1 / ((sin . x) #Z (n - 1)))) * (- ((cos . x) / ((sin . x) ^2))) by A7, Th3
.= (n / ((sin . x) #Z (n - 1))) * ((- (cos . x)) / ((sin . x) ^2))
.= (n * (- (cos . x))) / (((sin . x) #Z (n - 1)) * ((sin . x) ^2)) by XCMPLX_1:76
.= (n * (- (cos . x))) / (((sin . x) #Z (n - 1)) * ((sin . x) #Z 2)) by FDIFF_7:1
.= (n * (- (cos . x))) / ((sin . x) #Z ((n - 1) + 2)) by A4, A8, PREPOWER:44
.= (n * (- (cos . x))) / ((sin . x) #Z (n + 1)) ;
hence  (((#Z n) * cosec) `| Z) . x = - ((n * (cos . x)) / ((sin . x) #Z (n + 1))) ; ::_thesis: verum
end;
hence  ( (#Z n) * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * cosec) `| Z) . x = - ((n * (cos . x)) / ((sin . x) #Z (n + 1))) ) ) by A1, A5, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:22
for Z being open Subset of REAL st Z c= dom (sec - (id Z)) holds
( sec - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((sec - (id Z)) `| Z) . x = ((sin . x) - ((cos . x) ^2)) / ((cos . x) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sec - (id Z)) implies ( sec - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((sec - (id Z)) `| Z) . x = ((sin . x) - ((cos . x) ^2)) / ((cos . x) ^2) ) ) )
A1: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:18;
assume A2: Z c= dom (sec - (id Z)) ; ::_thesis: ( sec - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((sec - (id Z)) `| Z) . x = ((sin . x) - ((cos . x) ^2)) / ((cos . x) ^2) ) )
then A3: Z c= (dom sec) /\ (dom (id Z)) by VALUED_1:12;
then A4: Z c= dom sec by XBOOLE_1:18;
A5: Z c= dom (id Z) by A3, XBOOLE_1:18;
then A6: id Z is_differentiable_on Z by A1, FDIFF_1:23;
 for x being Real st x in Z holds
sec is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sec is_differentiable_in x )
assume  x in Z ; ::_thesis: sec is_differentiable_in x
then  cos . x <> 0 by A4, RFUNCT_1:3;
hence  sec is_differentiable_in x by Th1; ::_thesis: verum
end;
then A7: sec is_differentiable_on Z by A4, FDIFF_1:9;
 for x being Real st x in Z holds
((sec - (id Z)) `| Z) . x = ((sin . x) - ((cos . x) ^2)) / ((cos . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((sec - (id Z)) `| Z) . x = ((sin . x) - ((cos . x) ^2)) / ((cos . x) ^2) )
assume A8: x in Z ; ::_thesis: ((sec - (id Z)) `| Z) . x = ((sin . x) - ((cos . x) ^2)) / ((cos . x) ^2)
then A9: cos . x <> 0 by A4, RFUNCT_1:3;
then A10: (cos . x) ^2 > 0 by SQUARE_1:12;
((sec - (id Z)) `| Z) . x = (diff (sec,x)) - (diff ((id Z),x)) by A2, A6, A7, A8, FDIFF_1:19
.= ((sin . x) / ((cos . x) ^2)) - (diff ((id Z),x)) by A9, Th1
.= ((sin . x) / ((cos . x) ^2)) - (((id Z) `| Z) . x) by A6, A8, FDIFF_1:def_7
.= ((sin . x) / ((cos . x) ^2)) - 1 by A5, A1, A8, FDIFF_1:23
.= ((sin . x) / ((cos . x) ^2)) - (((cos . x) ^2) / ((cos . x) ^2)) by A10, XCMPLX_1:60
.= ((sin . x) - ((cos . x) ^2)) / ((cos . x) ^2) ;
hence  ((sec - (id Z)) `| Z) . x = ((sin . x) - ((cos . x) ^2)) / ((cos . x) ^2) ; ::_thesis: verum
end;
hence  ( sec - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((sec - (id Z)) `| Z) . x = ((sin . x) - ((cos . x) ^2)) / ((cos . x) ^2) ) ) by A2, A6, A7, FDIFF_1:19; ::_thesis: verum
end;

theorem :: FDIFF_9:23
for Z being open Subset of REAL st Z c= dom ((- cosec) - (id Z)) holds
( (- cosec) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cosec) - (id Z)) `| Z) . x = ((cos . x) - ((sin . x) ^2)) / ((sin . x) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((- cosec) - (id Z)) implies ( (- cosec) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cosec) - (id Z)) `| Z) . x = ((cos . x) - ((sin . x) ^2)) / ((sin . x) ^2) ) ) )
set f = - cosec;
A1: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:18;
assume A2: Z c= dom ((- cosec) - (id Z)) ; ::_thesis: ( (- cosec) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cosec) - (id Z)) `| Z) . x = ((cos . x) - ((sin . x) ^2)) / ((sin . x) ^2) ) )
then A3: Z c= (dom (- cosec)) /\ (dom (id Z)) by VALUED_1:12;
then A4: Z c= dom (- cosec) by XBOOLE_1:18;
then A5: Z c= dom cosec by VALUED_1:8;
 for x being Real st x in Z holds
cosec is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cosec is_differentiable_in x )
assume  x in Z ; ::_thesis: cosec is_differentiable_in x
then  sin . x <> 0 by A5, RFUNCT_1:3;
hence  cosec is_differentiable_in x by Th2; ::_thesis: verum
end;
then A6: cosec is_differentiable_on Z by A5, FDIFF_1:9;
then A7: (- 1) (#) cosec is_differentiable_on Z by A4, FDIFF_1:20;
A8: Z c= dom (id Z) by A3, XBOOLE_1:18;
then A9: id Z is_differentiable_on Z by A1, FDIFF_1:23;
 for x being Real st x in Z holds
(((- cosec) - (id Z)) `| Z) . x = ((cos . x) - ((sin . x) ^2)) / ((sin . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies (((- cosec) - (id Z)) `| Z) . x = ((cos . x) - ((sin . x) ^2)) / ((sin . x) ^2) )
assume A10: x in Z ; ::_thesis: (((- cosec) - (id Z)) `| Z) . x = ((cos . x) - ((sin . x) ^2)) / ((sin . x) ^2)
then A11: sin . x <> 0 by A5, RFUNCT_1:3;
then A12: (sin . x) ^2 > 0 by SQUARE_1:12;
(((- cosec) - (id Z)) `| Z) . x = (diff ((- cosec),x)) - (diff ((id Z),x)) by A2, A9, A7, A10, FDIFF_1:19
.= ((((- 1) (#) cosec) `| Z) . x) - (diff ((id Z),x)) by A7, A10, FDIFF_1:def_7
.= ((- 1) * (diff (cosec,x))) - (diff ((id Z),x)) by A4, A6, A10, FDIFF_1:20
.= ((- 1) * (- ((cos . x) / ((sin . x) ^2)))) - (diff ((id Z),x)) by A11, Th2
.= ((cos . x) / ((sin . x) ^2)) - (((id Z) `| Z) . x) by A9, A10, FDIFF_1:def_7
.= ((cos . x) / ((sin . x) ^2)) - 1 by A8, A1, A10, FDIFF_1:23
.= ((cos . x) / ((sin . x) ^2)) - (((sin . x) ^2) / ((sin . x) ^2)) by A12, XCMPLX_1:60
.= ((cos . x) - ((sin . x) ^2)) / ((sin . x) ^2) ;
hence  (((- cosec) - (id Z)) `| Z) . x = ((cos . x) - ((sin . x) ^2)) / ((sin . x) ^2) ; ::_thesis: verum
end;
hence  ( (- cosec) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cosec) - (id Z)) `| Z) . x = ((cos . x) - ((sin . x) ^2)) / ((sin . x) ^2) ) ) by A2, A9, A7, FDIFF_1:19; ::_thesis: verum
end;

theorem :: FDIFF_9:24
for Z being open Subset of REAL st Z c= dom (exp_R (#) sec) holds
( exp_R (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) sec) `| Z) . x = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R (#) sec) implies ( exp_R (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) sec) `| Z) . x = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) ) ) )
A1: for x being Real st x in Z holds
exp_R is_differentiable_in x by SIN_COS:65;
assume A2: Z c= dom (exp_R (#) sec) ; ::_thesis: ( exp_R (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) sec) `| Z) . x = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) ) )
then A3: Z c= (dom exp_R) /\ (dom sec) by VALUED_1:def_4;
then A4: Z c= dom sec by XBOOLE_1:18;
 Z c= dom exp_R by A3, XBOOLE_1:18;
then A5: exp_R is_differentiable_on Z by A1, FDIFF_1:9;
A6: for x being Real st x in Z holds
( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
proof
let x be Real; ::_thesis: ( x in Z implies ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) )
assume  x in Z ; ::_thesis: ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
then  cos . x <> 0 by A4, RFUNCT_1:3;
hence  ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) by Th1; ::_thesis: verum
end;
then  for x being Real st x in Z holds
sec is_differentiable_in x ;
then A7: sec is_differentiable_on Z by A4, FDIFF_1:9;
 for x being Real st x in Z holds
((exp_R (#) sec) `| Z) . x = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((exp_R (#) sec) `| Z) . x = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) )
assume A8: x in Z ; ::_thesis: ((exp_R (#) sec) `| Z) . x = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2))
then ((exp_R (#) sec) `| Z) . x = ((sec . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff (sec,x))) by A2, A5, A7, FDIFF_1:21
.= ((sec . x) * (exp_R . x)) + ((exp_R . x) * (diff (sec,x))) by SIN_COS:65
.= ((sec . x) * (exp_R . x)) + ((exp_R . x) * ((sin . x) / ((cos . x) ^2))) by A6, A8
.= ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) by A4, A8, RFUNCT_1:def_2 ;
hence  ((exp_R (#) sec) `| Z) . x = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) ; ::_thesis: verum
end;
hence  ( exp_R (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) sec) `| Z) . x = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) ) ) by A2, A5, A7, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_9:25
for Z being open Subset of REAL st Z c= dom (exp_R (#) cosec) holds
( exp_R (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) cosec) `| Z) . x = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R (#) cosec) implies ( exp_R (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) cosec) `| Z) . x = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) ) ) )
A1: for x being Real st x in Z holds
exp_R is_differentiable_in x by SIN_COS:65;
assume A2: Z c= dom (exp_R (#) cosec) ; ::_thesis: ( exp_R (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) cosec) `| Z) . x = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) ) )
then A3: Z c= (dom exp_R) /\ (dom cosec) by VALUED_1:def_4;
then A4: Z c= dom cosec by XBOOLE_1:18;
 Z c= dom exp_R by A3, XBOOLE_1:18;
then A5: exp_R is_differentiable_on Z by A1, FDIFF_1:9;
A6: for x being Real st x in Z holds
( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
proof
let x be Real; ::_thesis: ( x in Z implies ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) )
assume  x in Z ; ::_thesis: ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
then  sin . x <> 0 by A4, RFUNCT_1:3;
hence  ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) by Th2; ::_thesis: verum
end;
then  for x being Real st x in Z holds
cosec is_differentiable_in x ;
then A7: cosec is_differentiable_on Z by A4, FDIFF_1:9;
 for x being Real st x in Z holds
((exp_R (#) cosec) `| Z) . x = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((exp_R (#) cosec) `| Z) . x = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) )
assume A8: x in Z ; ::_thesis: ((exp_R (#) cosec) `| Z) . x = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2))
then ((exp_R (#) cosec) `| Z) . x = ((cosec . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff (cosec,x))) by A2, A5, A7, FDIFF_1:21
.= ((cosec . x) * (exp_R . x)) + ((exp_R . x) * (diff (cosec,x))) by SIN_COS:65
.= ((cosec . x) * (exp_R . x)) + ((exp_R . x) * (- ((cos . x) / ((sin . x) ^2)))) by A6, A8
.= ((exp_R . x) / (sin . x)) + (((exp_R . x) * (- (cos . x))) / ((sin . x) ^2)) by A4, A8, RFUNCT_1:def_2 ;
hence  ((exp_R (#) cosec) `| Z) . x = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) ; ::_thesis: verum
end;
hence  ( exp_R (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) cosec) `| Z) . x = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) ) ) by A2, A5, A7, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_9:26
for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (((1 / a) (#) (sec * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((1 / a) (#) (sec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / a) (#) (sec * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ) )
proof
let a be Real; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (((1 / a) (#) (sec * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((1 / a) (#) (sec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / a) (#) (sec * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ) )
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (((1 / a) (#) (sec * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((1 / a) (#) (sec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / a) (#) (sec * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (((1 / a) (#) (sec * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) implies ( ((1 / a) (#) (sec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / a) (#) (sec * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ) ) )
assume that
A1: Z c= dom (((1 / a) (#) (sec * f)) - (id Z)) and
A2: for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ; ::_thesis: ( ((1 / a) (#) (sec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / a) (#) (sec * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ) )
A3: Z c= (dom ((1 / a) (#) (sec * f))) /\ (dom (id Z)) by A1, VALUED_1:12;
then A4: Z c= dom ((1 / a) (#) (sec * f)) by XBOOLE_1:18;
then A5: Z c= dom (sec * f) by VALUED_1:def_5;
A6: for x being Real st x in Z holds
f . x = (a * x) + 0 by A2;
then A7: sec * f is_differentiable_on Z by A5, Th6;
then A8: (1 / a) (#) (sec * f) is_differentiable_on Z by A4, FDIFF_1:20;
set g = (1 / a) (#) (sec * f);
A9: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:18;
A10: Z c= dom (id Z) by A3, XBOOLE_1:18;
then A11: id Z is_differentiable_on Z by A9, FDIFF_1:23;
A12: for x being Real st x in Z holds
cos . (f . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies cos . (f . x) <> 0 )
assume  x in Z ; ::_thesis: cos . (f . x) <> 0
then  f . x in dom sec by A5, FUNCT_1:11;
hence  cos . (f . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
 for x being Real st x in Z holds
((((1 / a) (#) (sec * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((((1 / a) (#) (sec * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) )
assume A13: x in Z ; ::_thesis: ((((1 / a) (#) (sec * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2)
then A14: f . x = (a * x) + 0 by A2;
 cos . (f . x) <> 0 by A12, A13;
then A15: (cos . (a * x)) ^2 > 0 by A14, SQUARE_1:12;
((((1 / a) (#) (sec * f)) - (id Z)) `| Z) . x = (diff (((1 / a) (#) (sec * f)),x)) - (diff ((id Z),x)) by A1, A8, A11, A13, FDIFF_1:19
.= ((((1 / a) (#) (sec * f)) `| Z) . x) - (diff ((id Z),x)) by A8, A13, FDIFF_1:def_7
.= ((1 / a) * (diff ((sec * f),x))) - (diff ((id Z),x)) by A4, A7, A13, FDIFF_1:20
.= ((1 / a) * (((sec * f) `| Z) . x)) - (diff ((id Z),x)) by A7, A13, FDIFF_1:def_7
.= ((1 / a) * (((sec * f) `| Z) . x)) - (((id Z) `| Z) . x) by A11, A13, FDIFF_1:def_7
.= ((1 / a) * ((a * (sin . (a * x))) / ((cos . (a * x)) ^2))) - (((id Z) `| Z) . x) by A5, A6, A13, A14, Th6
.= ((1 / a) * ((a * (sin . (a * x))) / ((cos . (a * x)) ^2))) - 1 by A10, A9, A13, FDIFF_1:23
.= ((1 * (a * (sin . (a * x)))) / (a * ((cos . (a * x)) ^2))) - 1 by XCMPLX_1:76
.= ((sin . (a * x)) / ((cos . (a * x)) ^2)) - 1 by A2, A13, XCMPLX_1:91
.= ((sin . (a * x)) / ((cos . (a * x)) ^2)) - (((cos . (a * x)) ^2) / ((cos . (a * x)) ^2)) by A15, XCMPLX_1:60
.= ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ;
hence  ((((1 / a) (#) (sec * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ; ::_thesis: verum
end;
hence  ( ((1 / a) (#) (sec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / a) (#) (sec * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ) ) by A1, A8, A11, FDIFF_1:19; ::_thesis: verum
end;

theorem :: FDIFF_9:27
for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (((- (1 / a)) (#) (cosec * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((- (1 / a)) (#) (cosec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) )
proof
let a be Real; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (((- (1 / a)) (#) (cosec * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((- (1 / a)) (#) (cosec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) )
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (((- (1 / a)) (#) (cosec * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((- (1 / a)) (#) (cosec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (((- (1 / a)) (#) (cosec * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) implies ( ((- (1 / a)) (#) (cosec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) ) )
assume that
A1: Z c= dom (((- (1 / a)) (#) (cosec * f)) - (id Z)) and
A2: for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ; ::_thesis: ( ((- (1 / a)) (#) (cosec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) )
A3: Z c= (dom ((- (1 / a)) (#) (cosec * f))) /\ (dom (id Z)) by A1, VALUED_1:12;
then A4: Z c= dom ((- (1 / a)) (#) (cosec * f)) by XBOOLE_1:18;
then A5: Z c= dom (cosec * f) by VALUED_1:def_5;
A6: for x being Real st x in Z holds
f . x = (a * x) + 0 by A2;
then A7: cosec * f is_differentiable_on Z by A5, Th7;
then A8: (- (1 / a)) (#) (cosec * f) is_differentiable_on Z by A4, FDIFF_1:20;
set g = (- (1 / a)) (#) (cosec * f);
A9: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:18;
A10: Z c= dom (id Z) by A3, XBOOLE_1:18;
then A11: id Z is_differentiable_on Z by A9, FDIFF_1:23;
A12: for x being Real st x in Z holds
sin . (f . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . (f . x) <> 0 )
assume  x in Z ; ::_thesis: sin . (f . x) <> 0
then  f . x in dom cosec by A5, FUNCT_1:11;
hence  sin . (f . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
 for x being Real st x in Z holds
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) )
assume A13: x in Z ; ::_thesis: ((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2)
then A14: f . x = (a * x) + 0 by A2;
 sin . (f . x) <> 0 by A12, A13;
then A15: (sin . (a * x)) ^2 > 0 by A14, SQUARE_1:12;
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = (diff (((- (1 / a)) (#) (cosec * f)),x)) - (diff ((id Z),x)) by A1, A8, A11, A13, FDIFF_1:19
.= ((((- (1 / a)) (#) (cosec * f)) `| Z) . x) - (diff ((id Z),x)) by A8, A13, FDIFF_1:def_7
.= ((- (1 / a)) * (diff ((cosec * f),x))) - (diff ((id Z),x)) by A4, A7, A13, FDIFF_1:20
.= ((- (1 / a)) * (((cosec * f) `| Z) . x)) - (diff ((id Z),x)) by A7, A13, FDIFF_1:def_7
.= ((- (1 / a)) * (((cosec * f) `| Z) . x)) - (((id Z) `| Z) . x) by A11, A13, FDIFF_1:def_7
.= ((- (1 / a)) * (- ((a * (cos . (a * x))) / ((sin . (a * x)) ^2)))) - (((id Z) `| Z) . x) by A5, A6, A13, A14, Th7
.= (((- 1) / a) * ((a * (- (cos . (a * x)))) / ((sin . (a * x)) ^2))) - 1 by A10, A9, A13, FDIFF_1:23
.= (((- 1) * (a * (- (cos . (a * x))))) / (a * ((sin . (a * x)) ^2))) - 1 by XCMPLX_1:76
.= (((cos . (a * x)) * a) / (((sin . (a * x)) ^2) * a)) - 1
.= ((cos . (a * x)) / ((sin . (a * x)) ^2)) - 1 by A2, A13, XCMPLX_1:91
.= ((cos . (a * x)) / ((sin . (a * x)) ^2)) - (((sin . (a * x)) ^2) / ((sin . (a * x)) ^2)) by A15, XCMPLX_1:60
.= ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ;
hence  ((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ; ::_thesis: verum
end;
hence  ( ((- (1 / a)) (#) (cosec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) ) by A1, A8, A11, FDIFF_1:19; ::_thesis: verum
end;

theorem :: FDIFF_9:28
for a, b being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (f (#) sec) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( f (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) sec) `| Z) . x = (a / (cos . x)) + ((((a * x) + b) * (sin . x)) / ((cos . x) ^2)) ) )
proof
let a, b be Real; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (f (#) sec) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( f (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) sec) `| Z) . x = (a / (cos . x)) + ((((a * x) + b) * (sin . x)) / ((cos . x) ^2)) ) )
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (f (#) sec) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( f (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) sec) `| Z) . x = (a / (cos . x)) + ((((a * x) + b) * (sin . x)) / ((cos . x) ^2)) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f (#) sec) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) implies ( f (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) sec) `| Z) . x = (a / (cos . x)) + ((((a * x) + b) * (sin . x)) / ((cos . x) ^2)) ) ) )
assume that
A1: Z c= dom (f (#) sec) and
A2: for x being Real st x in Z holds
f . x = (a * x) + b ; ::_thesis: ( f (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) sec) `| Z) . x = (a / (cos . x)) + ((((a * x) + b) * (sin . x)) / ((cos . x) ^2)) ) )
A3: Z c= (dom f) /\ (dom sec) by A1, VALUED_1:def_4;
then A4: Z c= dom sec by XBOOLE_1:18;
A5: Z c= dom f by A3, XBOOLE_1:18;
then A6: f is_differentiable_on Z by A2, FDIFF_1:23;
A7: for x being Real st x in Z holds
( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
proof
let x be Real; ::_thesis: ( x in Z implies ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) )
assume  x in Z ; ::_thesis: ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
then  cos . x <> 0 by A4, RFUNCT_1:3;
hence  ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) by Th1; ::_thesis: verum
end;
then  for x being Real st x in Z holds
sec is_differentiable_in x ;
then A8: sec is_differentiable_on Z by A4, FDIFF_1:9;
 for x being Real st x in Z holds
((f (#) sec) `| Z) . x = (a / (cos . x)) + ((((a * x) + b) * (sin . x)) / ((cos . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((f (#) sec) `| Z) . x = (a / (cos . x)) + ((((a * x) + b) * (sin . x)) / ((cos . x) ^2)) )
assume A9: x in Z ; ::_thesis: ((f (#) sec) `| Z) . x = (a / (cos . x)) + ((((a * x) + b) * (sin . x)) / ((cos . x) ^2))
then ((f (#) sec) `| Z) . x = ((sec . x) * (diff (f,x))) + ((f . x) * (diff (sec,x))) by A1, A6, A8, FDIFF_1:21
.= ((sec . x) * ((f `| Z) . x)) + ((f . x) * (diff (sec,x))) by A6, A9, FDIFF_1:def_7
.= ((sec . x) * a) + ((f . x) * (diff (sec,x))) by A2, A5, A9, FDIFF_1:23
.= ((sec . x) * a) + (((a * x) + b) * (diff (sec,x))) by A2, A9
.= ((sec . x) * a) + (((a * x) + b) * ((sin . x) / ((cos . x) ^2))) by A7, A9
.= (a / (cos . x)) + ((((a * x) + b) * (sin . x)) / ((cos . x) ^2)) by A4, A9, RFUNCT_1:def_2 ;
hence  ((f (#) sec) `| Z) . x = (a / (cos . x)) + ((((a * x) + b) * (sin . x)) / ((cos . x) ^2)) ; ::_thesis: verum
end;
hence  ( f (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) sec) `| Z) . x = (a / (cos . x)) + ((((a * x) + b) * (sin . x)) / ((cos . x) ^2)) ) ) by A1, A6, A8, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_9:29
for a, b being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (f (#) cosec) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( f (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) cosec) `| Z) . x = (a / (sin . x)) - ((((a * x) + b) * (cos . x)) / ((sin . x) ^2)) ) )
proof
let a, b be Real; ::_thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (f (#) cosec) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( f (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) cosec) `| Z) . x = (a / (sin . x)) - ((((a * x) + b) * (cos . x)) / ((sin . x) ^2)) ) )
let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (f (#) cosec) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( f (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) cosec) `| Z) . x = (a / (sin . x)) - ((((a * x) + b) * (cos . x)) / ((sin . x) ^2)) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f (#) cosec) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) implies ( f (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) cosec) `| Z) . x = (a / (sin . x)) - ((((a * x) + b) * (cos . x)) / ((sin . x) ^2)) ) ) )
assume that
A1: Z c= dom (f (#) cosec) and
A2: for x being Real st x in Z holds
f . x = (a * x) + b ; ::_thesis: ( f (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) cosec) `| Z) . x = (a / (sin . x)) - ((((a * x) + b) * (cos . x)) / ((sin . x) ^2)) ) )
A3: Z c= (dom f) /\ (dom cosec) by A1, VALUED_1:def_4;
then A4: Z c= dom cosec by XBOOLE_1:18;
A5: Z c= dom f by A3, XBOOLE_1:18;
then A6: f is_differentiable_on Z by A2, FDIFF_1:23;
A7: for x being Real st x in Z holds
( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
proof
let x be Real; ::_thesis: ( x in Z implies ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) )
assume  x in Z ; ::_thesis: ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
then  sin . x <> 0 by A4, RFUNCT_1:3;
hence  ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) by Th2; ::_thesis: verum
end;
then  for x being Real st x in Z holds
cosec is_differentiable_in x ;
then A8: cosec is_differentiable_on Z by A4, FDIFF_1:9;
 for x being Real st x in Z holds
((f (#) cosec) `| Z) . x = (a / (sin . x)) - ((((a * x) + b) * (cos . x)) / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((f (#) cosec) `| Z) . x = (a / (sin . x)) - ((((a * x) + b) * (cos . x)) / ((sin . x) ^2)) )
assume A9: x in Z ; ::_thesis: ((f (#) cosec) `| Z) . x = (a / (sin . x)) - ((((a * x) + b) * (cos . x)) / ((sin . x) ^2))
then ((f (#) cosec) `| Z) . x = ((cosec . x) * (diff (f,x))) + ((f . x) * (diff (cosec,x))) by A1, A6, A8, FDIFF_1:21
.= ((cosec . x) * ((f `| Z) . x)) + ((f . x) * (diff (cosec,x))) by A6, A9, FDIFF_1:def_7
.= ((cosec . x) * a) + ((f . x) * (diff (cosec,x))) by A2, A5, A9, FDIFF_1:23
.= ((cosec . x) * a) + (((a * x) + b) * (diff (cosec,x))) by A2, A9
.= ((cosec . x) * a) + (((a * x) + b) * (- ((cos . x) / ((sin . x) ^2)))) by A7, A9
.= (a / (sin . x)) - ((((a * x) + b) * (cos . x)) / ((sin . x) ^2)) by A4, A9, RFUNCT_1:def_2 ;
hence  ((f (#) cosec) `| Z) . x = (a / (sin . x)) - ((((a * x) + b) * (cos . x)) / ((sin . x) ^2)) ; ::_thesis: verum
end;
hence  ( f (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((f (#) cosec) `| Z) . x = (a / (sin . x)) - ((((a * x) + b) * (cos . x)) / ((sin . x) ^2)) ) ) by A1, A6, A8, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_9:30
for Z being open Subset of REAL st Z c= dom (ln (#) sec) holds
( ln (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) sec) `| Z) . x = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln (#) sec) implies ( ln (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) sec) `| Z) . x = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) ) ) )
assume A1: Z c= dom (ln (#) sec) ; ::_thesis: ( ln (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) sec) `| Z) . x = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) ) )
then A2: Z c= (dom ln) /\ (dom sec) by VALUED_1:def_4;
then A3: Z c= dom sec by XBOOLE_1:18;
A4: for x being Real st x in Z holds
( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
proof
let x be Real; ::_thesis: ( x in Z implies ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) )
assume  x in Z ; ::_thesis: ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
then  cos . x <> 0 by A3, RFUNCT_1:3;
hence  ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) by Th1; ::_thesis: verum
end;
then  for x being Real st x in Z holds
sec is_differentiable_in x ;
then A5: sec is_differentiable_on Z by A3, FDIFF_1:9;
A6: Z c= dom ln by A2, XBOOLE_1:18;
A7: for x being Real st x in Z holds
x > 0
proof
let x be Real; ::_thesis: ( x in Z implies x > 0 )
assume  x in Z ; ::_thesis: x > 0
then  x in right_open_halfline 0 by A6, TAYLOR_1:18;
then  ex g being Real st
( x = g & 0 < g ) by Lm1;
hence  x > 0 ; ::_thesis: verum
end;
then  for x being Real st x in Z holds
ln is_differentiable_in x by TAYLOR_1:18;
then A8: ln is_differentiable_on Z by A6, FDIFF_1:9;
A9: for x being Real st x in Z holds
diff (ln,x) = 1 / x
proof
let x be Real; ::_thesis: ( x in Z implies diff (ln,x) = 1 / x )
assume  x in Z ; ::_thesis: diff (ln,x) = 1 / x
then  x > 0 by A7;
then  x in right_open_halfline 0 by Lm1;
hence  diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum
end;
 for x being Real st x in Z holds
((ln (#) sec) `| Z) . x = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((ln (#) sec) `| Z) . x = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) )
assume A10: x in Z ; ::_thesis: ((ln (#) sec) `| Z) . x = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2))
then ((ln (#) sec) `| Z) . x = ((sec . x) * (diff (ln,x))) + ((ln . x) * (diff (sec,x))) by A1, A8, A5, FDIFF_1:21
.= ((sec . x) * (1 / x)) + ((ln . x) * (diff (sec,x))) by A9, A10
.= ((sec . x) * (1 / x)) + ((ln . x) * ((sin . x) / ((cos . x) ^2))) by A4, A10
.= ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) by A3, A10, RFUNCT_1:def_2 ;
hence  ((ln (#) sec) `| Z) . x = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) ; ::_thesis: verum
end;
hence  ( ln (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) sec) `| Z) . x = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) ) ) by A1, A8, A5, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_9:31
for Z being open Subset of REAL st Z c= dom (ln (#) cosec) holds
( ln (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) cosec) `| Z) . x = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln (#) cosec) implies ( ln (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) cosec) `| Z) . x = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) ) ) )
assume A1: Z c= dom (ln (#) cosec) ; ::_thesis: ( ln (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) cosec) `| Z) . x = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) ) )
then A2: Z c= (dom ln) /\ (dom cosec) by VALUED_1:def_4;
then A3: Z c= dom cosec by XBOOLE_1:18;
A4: for x being Real st x in Z holds
( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
proof
let x be Real; ::_thesis: ( x in Z implies ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) )
assume  x in Z ; ::_thesis: ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
then  sin . x <> 0 by A3, RFUNCT_1:3;
hence  ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) by Th2; ::_thesis: verum
end;
then  for x being Real st x in Z holds
cosec is_differentiable_in x ;
then A5: cosec is_differentiable_on Z by A3, FDIFF_1:9;
A6: Z c= dom ln by A2, XBOOLE_1:18;
A7: for x being Real st x in Z holds
x > 0
proof
let x be Real; ::_thesis: ( x in Z implies x > 0 )
assume  x in Z ; ::_thesis: x > 0
then  x in right_open_halfline 0 by A6, TAYLOR_1:18;
then  ex g being Real st
( x = g & 0 < g ) by Lm1;
hence  x > 0 ; ::_thesis: verum
end;
then  for x being Real st x in Z holds
ln is_differentiable_in x by TAYLOR_1:18;
then A8: ln is_differentiable_on Z by A6, FDIFF_1:9;
A9: for x being Real st x in Z holds
diff (ln,x) = 1 / x
proof
let x be Real; ::_thesis: ( x in Z implies diff (ln,x) = 1 / x )
assume  x in Z ; ::_thesis: diff (ln,x) = 1 / x
then  x > 0 by A7;
then  x in right_open_halfline 0 by Lm1;
hence  diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum
end;
 for x being Real st x in Z holds
((ln (#) cosec) `| Z) . x = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((ln (#) cosec) `| Z) . x = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) )
assume A10: x in Z ; ::_thesis: ((ln (#) cosec) `| Z) . x = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2))
then ((ln (#) cosec) `| Z) . x = ((cosec . x) * (diff (ln,x))) + ((ln . x) * (diff (cosec,x))) by A1, A8, A5, FDIFF_1:21
.= ((cosec . x) * (1 / x)) + ((ln . x) * (diff (cosec,x))) by A9, A10
.= ((cosec . x) * (1 / x)) + ((ln . x) * (- ((cos . x) / ((sin . x) ^2)))) by A4, A10
.= ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) by A3, A10, RFUNCT_1:def_2 ;
hence  ((ln (#) cosec) `| Z) . x = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) ; ::_thesis: verum
end;
hence  ( ln (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) cosec) `| Z) . x = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) ) ) by A1, A8, A5, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_9:32
for Z being open Subset of REAL st not 0 in Z & Z c= dom (((id Z) ^) (#) sec) holds
( ((id Z) ^) (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) sec) `| Z) . x = (- ((1 / (cos . x)) / (x ^2))) + (((sin . x) / x) / ((cos . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & Z c= dom (((id Z) ^) (#) sec) implies ( ((id Z) ^) (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) sec) `| Z) . x = (- ((1 / (cos . x)) / (x ^2))) + (((sin . x) / x) / ((cos . x) ^2)) ) ) )
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (((id Z) ^) (#) sec) ; ::_thesis: ( ((id Z) ^) (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) sec) `| Z) . x = (- ((1 / (cos . x)) / (x ^2))) + (((sin . x) / x) / ((cos . x) ^2)) ) )
A3: (id Z) ^ is_differentiable_on Z by A1, FDIFF_5:4;
A4: Z c= (dom ((id Z) ^)) /\ (dom sec) by A2, VALUED_1:def_4;
then A5: Z c= dom sec by XBOOLE_1:18;
A6: for x being Real st x in Z holds
( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
proof
let x be Real; ::_thesis: ( x in Z implies ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) )
assume  x in Z ; ::_thesis: ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
then  cos . x <> 0 by A5, RFUNCT_1:3;
hence  ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) by Th1; ::_thesis: verum
end;
then  for x being Real st x in Z holds
sec is_differentiable_in x ;
then A7: sec is_differentiable_on Z by A5, FDIFF_1:9;
A8: Z c= dom ((id Z) ^) by A4, XBOOLE_1:18;
 for x being Real st x in Z holds
((((id Z) ^) (#) sec) `| Z) . x = (- ((1 / (cos . x)) / (x ^2))) + (((sin . x) / x) / ((cos . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((((id Z) ^) (#) sec) `| Z) . x = (- ((1 / (cos . x)) / (x ^2))) + (((sin . x) / x) / ((cos . x) ^2)) )
assume A9: x in Z ; ::_thesis: ((((id Z) ^) (#) sec) `| Z) . x = (- ((1 / (cos . x)) / (x ^2))) + (((sin . x) / x) / ((cos . x) ^2))
then ((((id Z) ^) (#) sec) `| Z) . x = ((sec . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff (sec,x))) by A2, A3, A7, FDIFF_1:21
.= ((sec . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff (sec,x))) by A3, A9, FDIFF_1:def_7
.= ((sec . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff (sec,x))) by A1, A9, FDIFF_5:4
.= (- ((sec . x) * (1 / (x ^2)))) + ((((id Z) ^) . x) * ((sin . x) / ((cos . x) ^2))) by A6, A9
.= (- (((cos . x) ") * (1 / (x ^2)))) + ((((id Z) ^) . x) * ((sin . x) / ((cos . x) ^2))) by A5, A9, RFUNCT_1:def_2
.= (- ((1 / (cos . x)) / (x ^2))) + ((((id Z) . x) ") * ((sin . x) / ((cos . x) ^2))) by A8, A9, RFUNCT_1:def_2
.= (- ((1 / (cos . x)) / (x ^2))) + ((1 / x) * ((sin . x) / ((cos . x) ^2))) by A9, FUNCT_1:18
.= (- ((1 / (cos . x)) / (x ^2))) + (((sin . x) / x) / ((cos . x) ^2)) ;
hence  ((((id Z) ^) (#) sec) `| Z) . x = (- ((1 / (cos . x)) / (x ^2))) + (((sin . x) / x) / ((cos . x) ^2)) ; ::_thesis: verum
end;
hence  ( ((id Z) ^) (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) sec) `| Z) . x = (- ((1 / (cos . x)) / (x ^2))) + (((sin . x) / x) / ((cos . x) ^2)) ) ) by A2, A3, A7, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_9:33
for Z being open Subset of REAL st not 0 in Z & Z c= dom (((id Z) ^) (#) cosec) holds
( ((id Z) ^) (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) cosec) `| Z) . x = (- ((1 / (sin . x)) / (x ^2))) - (((cos . x) / x) / ((sin . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & Z c= dom (((id Z) ^) (#) cosec) implies ( ((id Z) ^) (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) cosec) `| Z) . x = (- ((1 / (sin . x)) / (x ^2))) - (((cos . x) / x) / ((sin . x) ^2)) ) ) )
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (((id Z) ^) (#) cosec) ; ::_thesis: ( ((id Z) ^) (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) cosec) `| Z) . x = (- ((1 / (sin . x)) / (x ^2))) - (((cos . x) / x) / ((sin . x) ^2)) ) )
A3: (id Z) ^ is_differentiable_on Z by A1, FDIFF_5:4;
A4: Z c= (dom ((id Z) ^)) /\ (dom cosec) by A2, VALUED_1:def_4;
then A5: Z c= dom cosec by XBOOLE_1:18;
A6: for x being Real st x in Z holds
( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
proof
let x be Real; ::_thesis: ( x in Z implies ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) )
assume  x in Z ; ::_thesis: ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
then  sin . x <> 0 by A5, RFUNCT_1:3;
hence  ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) by Th2; ::_thesis: verum
end;
then  for x being Real st x in Z holds
cosec is_differentiable_in x ;
then A7: cosec is_differentiable_on Z by A5, FDIFF_1:9;
A8: Z c= dom ((id Z) ^) by A4, XBOOLE_1:18;
 for x being Real st x in Z holds
((((id Z) ^) (#) cosec) `| Z) . x = (- ((1 / (sin . x)) / (x ^2))) - (((cos . x) / x) / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((((id Z) ^) (#) cosec) `| Z) . x = (- ((1 / (sin . x)) / (x ^2))) - (((cos . x) / x) / ((sin . x) ^2)) )
assume A9: x in Z ; ::_thesis: ((((id Z) ^) (#) cosec) `| Z) . x = (- ((1 / (sin . x)) / (x ^2))) - (((cos . x) / x) / ((sin . x) ^2))
then ((((id Z) ^) (#) cosec) `| Z) . x = ((cosec . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff (cosec,x))) by A2, A3, A7, FDIFF_1:21
.= ((cosec . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff (cosec,x))) by A3, A9, FDIFF_1:def_7
.= ((cosec . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff (cosec,x))) by A1, A9, FDIFF_5:4
.= (- ((cosec . x) * (1 / (x ^2)))) + ((((id Z) ^) . x) * (- ((cos . x) / ((sin . x) ^2)))) by A6, A9
.= (- (((sin . x) ") * (1 / (x ^2)))) + ((((id Z) ^) . x) * ((- (cos . x)) / ((sin . x) ^2))) by A5, A9, RFUNCT_1:def_2
.= (- ((1 / (sin . x)) / (x ^2))) + ((((id Z) . x) ") * ((- (cos . x)) / ((sin . x) ^2))) by A8, A9, RFUNCT_1:def_2
.= (- ((1 / (sin . x)) / (x ^2))) + ((1 / x) * ((- (cos . x)) / ((sin . x) ^2))) by A9, FUNCT_1:18
.= (- ((1 / (sin . x)) / (x ^2))) + (((- (cos . x)) / x) / ((sin . x) ^2)) ;
hence  ((((id Z) ^) (#) cosec) `| Z) . x = (- ((1 / (sin . x)) / (x ^2))) - (((cos . x) / x) / ((sin . x) ^2)) ; ::_thesis: verum
end;
hence  ( ((id Z) ^) (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) cosec) `| Z) . x = (- ((1 / (sin . x)) / (x ^2))) - (((cos . x) / x) / ((sin . x) ^2)) ) ) by A2, A3, A7, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_9:34
for Z being open Subset of REAL st Z c= dom (sec * sin) holds
( sec * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * sin) `| Z) . x = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sec * sin) implies ( sec * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * sin) `| Z) . x = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) ) ) )
assume A1: Z c= dom (sec * sin) ; ::_thesis: ( sec * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * sin) `| Z) . x = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) ) )
A2: for x being Real st x in Z holds
cos . (sin . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies cos . (sin . x) <> 0 )
assume  x in Z ; ::_thesis: cos . (sin . x) <> 0
then  sin . x in dom sec by A1, FUNCT_1:11;
hence  cos . (sin . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A3: for x being Real st x in Z holds
sec * sin is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sec * sin is_differentiable_in x )
assume  x in Z ; ::_thesis: sec * sin is_differentiable_in x
then  cos . (sin . x) <> 0 by A2;
then  ( sin is_differentiable_in x & sec is_differentiable_in sin . x ) by Th1, SIN_COS:64;
hence  sec * sin is_differentiable_in x by FDIFF_2:13; ::_thesis: verum
end;
then A4: sec * sin is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sec * sin) `| Z) . x = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((sec * sin) `| Z) . x = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) )
assume A5: x in Z ; ::_thesis: ((sec * sin) `| Z) . x = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2)
then A6: cos . (sin . x) <> 0 by A2;
then  ( sin is_differentiable_in x & sec is_differentiable_in sin . x ) by Th1, SIN_COS:64;
then  diff ((sec * sin),x) = (diff (sec,(sin . x))) * (diff (sin,x)) by FDIFF_2:13
.= ((sin . (sin . x)) / ((cos . (sin . x)) ^2)) * (diff (sin,x)) by A6, Th1
.= (cos . x) * ((sin . (sin . x)) / ((cos . (sin . x)) ^2)) by SIN_COS:64 ;
hence  ((sec * sin) `| Z) . x = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) by A4, A5, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sec * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * sin) `| Z) . x = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:35
for Z being open Subset of REAL st Z c= dom (sec * cos) holds
( sec * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * cos) `| Z) . x = - (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sec * cos) implies ( sec * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * cos) `| Z) . x = - (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2)) ) ) )
assume A1: Z c= dom (sec * cos) ; ::_thesis: ( sec * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * cos) `| Z) . x = - (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2)) ) )
A2: for x being Real st x in Z holds
cos . (cos . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies cos . (cos . x) <> 0 )
assume  x in Z ; ::_thesis: cos . (cos . x) <> 0
then  cos . x in dom sec by A1, FUNCT_1:11;
hence  cos . (cos . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A3: for x being Real st x in Z holds
sec * cos is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sec * cos is_differentiable_in x )
assume  x in Z ; ::_thesis: sec * cos is_differentiable_in x
then  cos . (cos . x) <> 0 by A2;
then  ( cos is_differentiable_in x & sec is_differentiable_in cos . x ) by Th1, SIN_COS:63;
hence  sec * cos is_differentiable_in x by FDIFF_2:13; ::_thesis: verum
end;
then A4: sec * cos is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sec * cos) `| Z) . x = - (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((sec * cos) `| Z) . x = - (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2)) )
assume A5: x in Z ; ::_thesis: ((sec * cos) `| Z) . x = - (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2))
then A6: cos . (cos . x) <> 0 by A2;
then  ( cos is_differentiable_in x & sec is_differentiable_in cos . x ) by Th1, SIN_COS:63;
then  diff ((sec * cos),x) = (diff (sec,(cos . x))) * (diff (cos,x)) by FDIFF_2:13
.= ((sin . (cos . x)) / ((cos . (cos . x)) ^2)) * (diff (cos,x)) by A6, Th1
.= (- (sin . x)) * ((sin . (cos . x)) / ((cos . (cos . x)) ^2)) by SIN_COS:63 ;
hence  ((sec * cos) `| Z) . x = - (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2)) by A4, A5, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sec * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * cos) `| Z) . x = - (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2)) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:36
for Z being open Subset of REAL st Z c= dom (cosec * sin) holds
( cosec * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * sin) `| Z) . x = - (((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cosec * sin) implies ( cosec * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * sin) `| Z) . x = - (((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2)) ) ) )
assume A1: Z c= dom (cosec * sin) ; ::_thesis: ( cosec * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * sin) `| Z) . x = - (((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2)) ) )
A2: for x being Real st x in Z holds
sin . (sin . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . (sin . x) <> 0 )
assume  x in Z ; ::_thesis: sin . (sin . x) <> 0
then  sin . x in dom cosec by A1, FUNCT_1:11;
hence  sin . (sin . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A3: for x being Real st x in Z holds
cosec * sin is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cosec * sin is_differentiable_in x )
assume  x in Z ; ::_thesis: cosec * sin is_differentiable_in x
then  sin . (sin . x) <> 0 by A2;
then  ( sin is_differentiable_in x & cosec is_differentiable_in sin . x ) by Th2, SIN_COS:64;
hence  cosec * sin is_differentiable_in x by FDIFF_2:13; ::_thesis: verum
end;
then A4: cosec * sin is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cosec * sin) `| Z) . x = - (((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((cosec * sin) `| Z) . x = - (((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2)) )
assume A5: x in Z ; ::_thesis: ((cosec * sin) `| Z) . x = - (((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2))
then A6: sin . (sin . x) <> 0 by A2;
then  ( sin is_differentiable_in x & cosec is_differentiable_in sin . x ) by Th2, SIN_COS:64;
then  diff ((cosec * sin),x) = (diff (cosec,(sin . x))) * (diff (sin,x)) by FDIFF_2:13
.= (- ((cos . (sin . x)) / ((sin . (sin . x)) ^2))) * (diff (sin,x)) by A6, Th2
.= (cos . x) * (- ((cos . (sin . x)) / ((sin . (sin . x)) ^2))) by SIN_COS:64 ;
hence  ((cosec * sin) `| Z) . x = - (((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2)) by A4, A5, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cosec * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * sin) `| Z) . x = - (((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2)) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:37
for Z being open Subset of REAL st Z c= dom (cosec * cos) holds
( cosec * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * cos) `| Z) . x = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cosec * cos) implies ( cosec * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * cos) `| Z) . x = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) ) ) )
assume A1: Z c= dom (cosec * cos) ; ::_thesis: ( cosec * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * cos) `| Z) . x = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) ) )
A2: for x being Real st x in Z holds
sin . (cos . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . (cos . x) <> 0 )
assume  x in Z ; ::_thesis: sin . (cos . x) <> 0
then  cos . x in dom cosec by A1, FUNCT_1:11;
hence  sin . (cos . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
A3: for x being Real st x in Z holds
cosec * cos is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cosec * cos is_differentiable_in x )
assume  x in Z ; ::_thesis: cosec * cos is_differentiable_in x
then  sin . (cos . x) <> 0 by A2;
then  ( cos is_differentiable_in x & cosec is_differentiable_in cos . x ) by Th2, SIN_COS:63;
hence  cosec * cos is_differentiable_in x by FDIFF_2:13; ::_thesis: verum
end;
then A4: cosec * cos is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cosec * cos) `| Z) . x = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((cosec * cos) `| Z) . x = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) )
assume A5: x in Z ; ::_thesis: ((cosec * cos) `| Z) . x = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2)
then A6: sin . (cos . x) <> 0 by A2;
then  ( cos is_differentiable_in x & cosec is_differentiable_in cos . x ) by Th2, SIN_COS:63;
then  diff ((cosec * cos),x) = (diff (cosec,(cos . x))) * (diff (cos,x)) by FDIFF_2:13
.= (- ((cos . (cos . x)) / ((sin . (cos . x)) ^2))) * (diff (cos,x)) by A6, Th2
.= (- (sin . x)) * (- ((cos . (cos . x)) / ((sin . (cos . x)) ^2))) by SIN_COS:63 ;
hence  ((cosec * cos) `| Z) . x = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) by A4, A5, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cosec * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * cos) `| Z) . x = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:38
for Z being open Subset of REAL st Z c= dom (sec * tan) holds
( sec * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * tan) `| Z) . x = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sec * tan) implies ( sec * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * tan) `| Z) . x = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) ) ) )
assume A1: Z c= dom (sec * tan) ; ::_thesis: ( sec * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * tan) `| Z) . x = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) ) )
A2: for x being Real st x in Z holds
cos . (tan . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies cos . (tan . x) <> 0 )
assume  x in Z ; ::_thesis: cos . (tan . x) <> 0
then  tan . x in dom sec by A1, FUNCT_1:11;
hence  cos . (tan . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
 dom (sec * tan) c= dom tan by RELAT_1:25;
then A3: Z c= dom tan by A1, XBOOLE_1:1;
A4: for x being Real st x in Z holds
sec * tan is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sec * tan is_differentiable_in x )
assume A5: x in Z ; ::_thesis: sec * tan is_differentiable_in x
then  cos . x <> 0 by A3, FDIFF_8:1;
then A6: tan is_differentiable_in x by FDIFF_7:46;
 cos . (tan . x) <> 0 by A2, A5;
then  sec is_differentiable_in tan . x by Th1;
hence  sec * tan is_differentiable_in x by A6, FDIFF_2:13; ::_thesis: verum
end;
then A7: sec * tan is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sec * tan) `| Z) . x = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((sec * tan) `| Z) . x = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) )
assume A8: x in Z ; ::_thesis: ((sec * tan) `| Z) . x = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2)
then A9: cos . x <> 0 by A3, FDIFF_8:1;
then A10: tan is_differentiable_in x by FDIFF_7:46;
A11: cos . (tan . x) <> 0 by A2, A8;
then  sec is_differentiable_in tan . x by Th1;
then  diff ((sec * tan),x) = (diff (sec,(tan . x))) * (diff (tan,x)) by A10, FDIFF_2:13
.= ((sin . (tan . x)) / ((cos . (tan . x)) ^2)) * (diff (tan,x)) by A11, Th1
.= (1 / ((cos . x) ^2)) * ((sin . (tan . x)) / ((cos . (tan . x)) ^2)) by A9, FDIFF_7:46
.= ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) ;
hence  ((sec * tan) `| Z) . x = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) by A7, A8, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sec * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * tan) `| Z) . x = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:39
for Z being open Subset of REAL st Z c= dom (sec * cot) holds
( sec * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * cot) `| Z) . x = - (((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sec * cot) implies ( sec * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * cot) `| Z) . x = - (((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2)) ) ) )
assume A1: Z c= dom (sec * cot) ; ::_thesis: ( sec * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * cot) `| Z) . x = - (((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2)) ) )
A2: for x being Real st x in Z holds
cos . (cot . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies cos . (cot . x) <> 0 )
assume  x in Z ; ::_thesis: cos . (cot . x) <> 0
then  cot . x in dom sec by A1, FUNCT_1:11;
hence  cos . (cot . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
 dom (sec * cot) c= dom cot by RELAT_1:25;
then A3: Z c= dom cot by A1, XBOOLE_1:1;
A4: for x being Real st x in Z holds
sec * cot is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sec * cot is_differentiable_in x )
assume A5: x in Z ; ::_thesis: sec * cot is_differentiable_in x
then  sin . x <> 0 by A3, FDIFF_8:2;
then A6: cot is_differentiable_in x by FDIFF_7:47;
 cos . (cot . x) <> 0 by A2, A5;
then  sec is_differentiable_in cot . x by Th1;
hence  sec * cot is_differentiable_in x by A6, FDIFF_2:13; ::_thesis: verum
end;
then A7: sec * cot is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sec * cot) `| Z) . x = - (((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((sec * cot) `| Z) . x = - (((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2)) )
assume A8: x in Z ; ::_thesis: ((sec * cot) `| Z) . x = - (((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2))
then A9: sin . x <> 0 by A3, FDIFF_8:2;
then A10: cot is_differentiable_in x by FDIFF_7:47;
A11: cos . (cot . x) <> 0 by A2, A8;
then  sec is_differentiable_in cot . x by Th1;
then  diff ((sec * cot),x) = (diff (sec,(cot . x))) * (diff (cot,x)) by A10, FDIFF_2:13
.= ((sin . (cot . x)) / ((cos . (cot . x)) ^2)) * (diff (cot,x)) by A11, Th1
.= (- (1 / ((sin . x) ^2))) * ((sin . (cot . x)) / ((cos . (cot . x)) ^2)) by A9, FDIFF_7:47
.= - (((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2)) ;
hence  ((sec * cot) `| Z) . x = - (((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2)) by A7, A8, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sec * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * cot) `| Z) . x = - (((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2)) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:40
for Z being open Subset of REAL st Z c= dom (cosec * tan) holds
( cosec * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * tan) `| Z) . x = - (((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cosec * tan) implies ( cosec * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * tan) `| Z) . x = - (((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2)) ) ) )
assume A1: Z c= dom (cosec * tan) ; ::_thesis: ( cosec * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * tan) `| Z) . x = - (((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2)) ) )
A2: for x being Real st x in Z holds
sin . (tan . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . (tan . x) <> 0 )
assume  x in Z ; ::_thesis: sin . (tan . x) <> 0
then  tan . x in dom cosec by A1, FUNCT_1:11;
hence  sin . (tan . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
 dom (cosec * tan) c= dom tan by RELAT_1:25;
then A3: Z c= dom tan by A1, XBOOLE_1:1;
A4: for x being Real st x in Z holds
cosec * tan is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cosec * tan is_differentiable_in x )
assume A5: x in Z ; ::_thesis: cosec * tan is_differentiable_in x
then  cos . x <> 0 by A3, FDIFF_8:1;
then A6: tan is_differentiable_in x by FDIFF_7:46;
 sin . (tan . x) <> 0 by A2, A5;
then  cosec is_differentiable_in tan . x by Th2;
hence  cosec * tan is_differentiable_in x by A6, FDIFF_2:13; ::_thesis: verum
end;
then A7: cosec * tan is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cosec * tan) `| Z) . x = - (((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((cosec * tan) `| Z) . x = - (((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2)) )
assume A8: x in Z ; ::_thesis: ((cosec * tan) `| Z) . x = - (((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2))
then A9: cos . x <> 0 by A3, FDIFF_8:1;
then A10: tan is_differentiable_in x by FDIFF_7:46;
A11: sin . (tan . x) <> 0 by A2, A8;
then  cosec is_differentiable_in tan . x by Th2;
then  diff ((cosec * tan),x) = (diff (cosec,(tan . x))) * (diff (tan,x)) by A10, FDIFF_2:13
.= (- ((cos . (tan . x)) / ((sin . (tan . x)) ^2))) * (diff (tan,x)) by A11, Th2
.= (1 / ((cos . x) ^2)) * (- ((cos . (tan . x)) / ((sin . (tan . x)) ^2))) by A9, FDIFF_7:46
.= - (((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2)) ;
hence  ((cosec * tan) `| Z) . x = - (((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2)) by A7, A8, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cosec * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * tan) `| Z) . x = - (((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2)) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:41
for Z being open Subset of REAL st Z c= dom (cosec * cot) holds
( cosec * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * cot) `| Z) . x = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cosec * cot) implies ( cosec * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * cot) `| Z) . x = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) ) ) )
assume A1: Z c= dom (cosec * cot) ; ::_thesis: ( cosec * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * cot) `| Z) . x = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) ) )
A2: for x being Real st x in Z holds
sin . (cot . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . (cot . x) <> 0 )
assume  x in Z ; ::_thesis: sin . (cot . x) <> 0
then  cot . x in dom cosec by A1, FUNCT_1:11;
hence  sin . (cot . x) <> 0 by RFUNCT_1:3; ::_thesis: verum
end;
 dom (cosec * cot) c= dom cot by RELAT_1:25;
then A3: Z c= dom cot by A1, XBOOLE_1:1;
A4: for x being Real st x in Z holds
cosec * cot is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cosec * cot is_differentiable_in x )
assume A5: x in Z ; ::_thesis: cosec * cot is_differentiable_in x
then  sin . x <> 0 by A3, FDIFF_8:2;
then A6: cot is_differentiable_in x by FDIFF_7:47;
 sin . (cot . x) <> 0 by A2, A5;
then  cosec is_differentiable_in cot . x by Th2;
hence  cosec * cot is_differentiable_in x by A6, FDIFF_2:13; ::_thesis: verum
end;
then A7: cosec * cot is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cosec * cot) `| Z) . x = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((cosec * cot) `| Z) . x = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) )
assume A8: x in Z ; ::_thesis: ((cosec * cot) `| Z) . x = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2)
then A9: sin . x <> 0 by A3, FDIFF_8:2;
then A10: cot is_differentiable_in x by FDIFF_7:47;
A11: sin . (cot . x) <> 0 by A2, A8;
then  cosec is_differentiable_in cot . x by Th2;
then  diff ((cosec * cot),x) = (diff (cosec,(cot . x))) * (diff (cot,x)) by A10, FDIFF_2:13
.= (- ((cos . (cot . x)) / ((sin . (cot . x)) ^2))) * (diff (cot,x)) by A11, Th2
.= (- (1 / ((sin . x) ^2))) * (- ((cos . (cot . x)) / ((sin . (cot . x)) ^2))) by A9, FDIFF_7:47
.= ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) ;
hence  ((cosec * cot) `| Z) . x = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) by A7, A8, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cosec * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * cot) `| Z) . x = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_9:42
for Z being open Subset of REAL st Z c= dom (tan (#) sec) holds
( tan (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((tan (#) sec) `| Z) . x = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (tan (#) sec) implies ( tan (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((tan (#) sec) `| Z) . x = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) ) ) )
assume A1: Z c= dom (tan (#) sec) ; ::_thesis: ( tan (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((tan (#) sec) `| Z) . x = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) ) )
then A2: Z c= (dom tan) /\ (dom sec) by VALUED_1:def_4;
then A3: Z c= dom tan by XBOOLE_1:18;
 for x being Real st x in Z holds
tan is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies tan is_differentiable_in x )
assume  x in Z ; ::_thesis: tan is_differentiable_in x
then  cos . x <> 0 by A3, FDIFF_8:1;
hence  tan is_differentiable_in x by FDIFF_7:46; ::_thesis: verum
end;
then A4: tan is_differentiable_on Z by A3, FDIFF_1:9;
A5: Z c= dom sec by A2, XBOOLE_1:18;
A6: for x being Real st x in Z holds
( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
proof
let x be Real; ::_thesis: ( x in Z implies ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) )
assume  x in Z ; ::_thesis: ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
then  cos . x <> 0 by A5, RFUNCT_1:3;
hence  ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) by Th1; ::_thesis: verum
end;
then  for x being Real st x in Z holds
sec is_differentiable_in x ;
then A7: sec is_differentiable_on Z by A5, FDIFF_1:9;
 for x being Real st x in Z holds
((tan (#) sec) `| Z) . x = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((tan (#) sec) `| Z) . x = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) )
assume A8: x in Z ; ::_thesis: ((tan (#) sec) `| Z) . x = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2))
then A9: cos . x <> 0 by A3, FDIFF_8:1;
((tan (#) sec) `| Z) . x = ((sec . x) * (diff (tan,x))) + ((tan . x) * (diff (sec,x))) by A1, A4, A7, A8, FDIFF_1:21
.= ((sec . x) * (1 / ((cos . x) ^2))) + ((tan . x) * (diff (sec,x))) by A9, FDIFF_7:46
.= ((sec . x) * (1 / ((cos . x) ^2))) + ((tan . x) * ((sin . x) / ((cos . x) ^2))) by A6, A8
.= ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) by A5, A8, RFUNCT_1:def_2 ;
hence  ((tan (#) sec) `| Z) . x = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) ; ::_thesis: verum
end;
hence  ( tan (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((tan (#) sec) `| Z) . x = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) ) ) by A1, A4, A7, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_9:43
for Z being open Subset of REAL st Z c= dom (cot (#) sec) holds
( cot (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((cot (#) sec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (cos . x))) + (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cot (#) sec) implies ( cot (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((cot (#) sec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (cos . x))) + (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) ) )
assume A1: Z c= dom (cot (#) sec) ; ::_thesis: ( cot (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((cot (#) sec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (cos . x))) + (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) )
then A2: Z c= (dom cot) /\ (dom sec) by VALUED_1:def_4;
then A3: Z c= dom cot by XBOOLE_1:18;
 for x being Real st x in Z holds
cot is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cot is_differentiable_in x )
assume  x in Z ; ::_thesis: cot is_differentiable_in x
then  sin . x <> 0 by A3, FDIFF_8:2;
hence  cot is_differentiable_in x by FDIFF_7:47; ::_thesis: verum
end;
then A4: cot is_differentiable_on Z by A3, FDIFF_1:9;
A5: Z c= dom sec by A2, XBOOLE_1:18;
A6: for x being Real st x in Z holds
( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
proof
let x be Real; ::_thesis: ( x in Z implies ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) )
assume  x in Z ; ::_thesis: ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
then  cos . x <> 0 by A5, RFUNCT_1:3;
hence  ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) by Th1; ::_thesis: verum
end;
then  for x being Real st x in Z holds
sec is_differentiable_in x ;
then A7: sec is_differentiable_on Z by A5, FDIFF_1:9;
 for x being Real st x in Z holds
((cot (#) sec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (cos . x))) + (((cot . x) * (sin . x)) / ((cos . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((cot (#) sec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (cos . x))) + (((cot . x) * (sin . x)) / ((cos . x) ^2)) )
assume A8: x in Z ; ::_thesis: ((cot (#) sec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (cos . x))) + (((cot . x) * (sin . x)) / ((cos . x) ^2))
then A9: sin . x <> 0 by A3, FDIFF_8:2;
((cot (#) sec) `| Z) . x = ((sec . x) * (diff (cot,x))) + ((cot . x) * (diff (sec,x))) by A1, A4, A7, A8, FDIFF_1:21
.= ((sec . x) * (- (1 / ((sin . x) ^2)))) + ((cot . x) * (diff (sec,x))) by A9, FDIFF_7:47
.= ((sec . x) * (- (1 / ((sin . x) ^2)))) + ((cot . x) * ((sin . x) / ((cos . x) ^2))) by A6, A8
.= ((- (1 / ((sin . x) ^2))) / (cos . x)) + (((cot . x) * (sin . x)) / ((cos . x) ^2)) by A5, A8, RFUNCT_1:def_2 ;
hence  ((cot (#) sec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (cos . x))) + (((cot . x) * (sin . x)) / ((cos . x) ^2)) ; ::_thesis: verum
end;
hence  ( cot (#) sec is_differentiable_on Z & ( for x being Real st x in Z holds
((cot (#) sec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (cos . x))) + (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) ) by A1, A4, A7, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_9:44
for Z being open Subset of REAL st Z c= dom (tan (#) cosec) holds
( tan (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((tan (#) cosec) `| Z) . x = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (tan (#) cosec) implies ( tan (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((tan (#) cosec) `| Z) . x = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) ) ) )
assume A1: Z c= dom (tan (#) cosec) ; ::_thesis: ( tan (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((tan (#) cosec) `| Z) . x = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) ) )
then A2: Z c= (dom tan) /\ (dom cosec) by VALUED_1:def_4;
then A3: Z c= dom tan by XBOOLE_1:18;
 for x being Real st x in Z holds
tan is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies tan is_differentiable_in x )
assume  x in Z ; ::_thesis: tan is_differentiable_in x
then  cos . x <> 0 by A3, FDIFF_8:1;
hence  tan is_differentiable_in x by FDIFF_7:46; ::_thesis: verum
end;
then A4: tan is_differentiable_on Z by A3, FDIFF_1:9;
A5: Z c= dom cosec by A2, XBOOLE_1:18;
A6: for x being Real st x in Z holds
( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
proof
let x be Real; ::_thesis: ( x in Z implies ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) )
assume  x in Z ; ::_thesis: ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
then  sin . x <> 0 by A5, RFUNCT_1:3;
hence  ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) by Th2; ::_thesis: verum
end;
then  for x being Real st x in Z holds
cosec is_differentiable_in x ;
then A7: cosec is_differentiable_on Z by A5, FDIFF_1:9;
 for x being Real st x in Z holds
((tan (#) cosec) `| Z) . x = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((tan (#) cosec) `| Z) . x = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) )
assume A8: x in Z ; ::_thesis: ((tan (#) cosec) `| Z) . x = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2))
then A9: cos . x <> 0 by A3, FDIFF_8:1;
((tan (#) cosec) `| Z) . x = ((cosec . x) * (diff (tan,x))) + ((tan . x) * (diff (cosec,x))) by A1, A4, A7, A8, FDIFF_1:21
.= ((cosec . x) * (1 / ((cos . x) ^2))) + ((tan . x) * (diff (cosec,x))) by A9, FDIFF_7:46
.= ((cosec . x) * (1 / ((cos . x) ^2))) + ((tan . x) * (- ((cos . x) / ((sin . x) ^2)))) by A6, A8
.= ((1 / ((cos . x) ^2)) / (sin . x)) + ((tan . x) * (- ((cos . x) / ((sin . x) ^2)))) by A5, A8, RFUNCT_1:def_2 ;
hence  ((tan (#) cosec) `| Z) . x = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) ; ::_thesis: verum
end;
hence  ( tan (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((tan (#) cosec) `| Z) . x = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) ) ) by A1, A4, A7, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_9:45
for Z being open Subset of REAL st Z c= dom (cot (#) cosec) holds
( cot (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((cot (#) cosec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (sin . x))) - (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cot (#) cosec) implies ( cot (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((cot (#) cosec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (sin . x))) - (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) ) )
assume A1: Z c= dom (cot (#) cosec) ; ::_thesis: ( cot (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((cot (#) cosec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (sin . x))) - (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) )
then A2: Z c= (dom cot) /\ (dom cosec) by VALUED_1:def_4;
then A3: Z c= dom cot by XBOOLE_1:18;
 for x being Real st x in Z holds
cot is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cot is_differentiable_in x )
assume  x in Z ; ::_thesis: cot is_differentiable_in x
then  sin . x <> 0 by A3, FDIFF_8:2;
hence  cot is_differentiable_in x by FDIFF_7:47; ::_thesis: verum
end;
then A4: cot is_differentiable_on Z by A3, FDIFF_1:9;
A5: Z c= dom cosec by A2, XBOOLE_1:18;
A6: for x being Real st x in Z holds
( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
proof
let x be Real; ::_thesis: ( x in Z implies ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) )
assume  x in Z ; ::_thesis: ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
then  sin . x <> 0 by A5, RFUNCT_1:3;
hence  ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) by Th2; ::_thesis: verum
end;
then  for x being Real st x in Z holds
cosec is_differentiable_in x ;
then A7: cosec is_differentiable_on Z by A5, FDIFF_1:9;
 for x being Real st x in Z holds
((cot (#) cosec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (sin . x))) - (((cot . x) * (cos . x)) / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((cot (#) cosec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (sin . x))) - (((cot . x) * (cos . x)) / ((sin . x) ^2)) )
assume A8: x in Z ; ::_thesis: ((cot (#) cosec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (sin . x))) - (((cot . x) * (cos . x)) / ((sin . x) ^2))
then A9: sin . x <> 0 by A3, FDIFF_8:2;
((cot (#) cosec) `| Z) . x = ((cosec . x) * (diff (cot,x))) + ((cot . x) * (diff (cosec,x))) by A1, A4, A7, A8, FDIFF_1:21
.= ((cosec . x) * (- (1 / ((sin . x) ^2)))) + ((cot . x) * (diff (cosec,x))) by A9, FDIFF_7:47
.= ((cosec . x) * (- (1 / ((sin . x) ^2)))) + ((cot . x) * (- ((cos . x) / ((sin . x) ^2)))) by A6, A8
.= ((- (1 / ((sin . x) ^2))) / (sin . x)) + ((cot . x) * (- ((cos . x) / ((sin . x) ^2)))) by A5, A8, RFUNCT_1:def_2 ;
hence  ((cot (#) cosec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (sin . x))) - (((cot . x) * (cos . x)) / ((sin . x) ^2)) ; ::_thesis: verum
end;
hence  ( cot (#) cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((cot (#) cosec) `| Z) . x = (- ((1 / ((sin . x) ^2)) / (sin . x))) - (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) ) by A1, A4, A7, FDIFF_1:21; ::_thesis: verum
end;