:: FDIFF_10 semantic presentation

begin


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

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

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

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

theorem Th5: :: FDIFF_10:5
for Z being open Subset of REAL st Z c= dom (tan - cot) holds
( tan - cot is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (tan - cot) implies ( tan - cot is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) ) )
assume A1: Z c= dom (tan - cot) ; ::_thesis: ( tan - cot is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) )
then A2: Z c= (dom tan) /\ (dom cot) by VALUED_1:12;
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 cot by A2, 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 A5, FDIFF_8:2;
hence  cot is_differentiable_in x by FDIFF_7:47; ::_thesis: verum
end;
then A6: cot is_differentiable_on Z by A5, FDIFF_1:9;
 for x being Real st x in Z holds
((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) )
assume A7: x in Z ; ::_thesis: ((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))
then A8: sin . x <> 0 by A5, FDIFF_8:2;
A9: cos . x <> 0 by A3, A7, FDIFF_8:1;
((tan - cot) `| Z) . x = (diff (tan,x)) - (diff (cot,x)) by A1, A6, A4, A7, FDIFF_1:19
.= (1 / ((cos . x) ^2)) - (diff (cot,x)) by A9, FDIFF_7:46
.= (1 / ((cos . x) ^2)) - (- (1 / ((sin . x) ^2))) by A8, FDIFF_7:47
.= (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ;
hence  ((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ; ::_thesis: verum
end;
hence  ( tan - cot is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) ) by A1, A6, A4, FDIFF_1:19; ::_thesis: verum
end;

theorem Th6: :: FDIFF_10:6
for Z being open Subset of REAL st Z c= dom (tan + cot) holds
( tan + cot is_differentiable_on Z & ( for x being Real st x in Z holds
((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (tan + cot) implies ( tan + cot is_differentiable_on Z & ( for x being Real st x in Z holds
((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) ) )
assume A1: Z c= dom (tan + cot) ; ::_thesis: ( tan + cot is_differentiable_on Z & ( for x being Real st x in Z holds
((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) )
then A2: Z c= (dom tan) /\ (dom cot) by VALUED_1:def_1;
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 cot by A2, 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 A5, FDIFF_8:2;
hence  cot is_differentiable_in x by FDIFF_7:47; ::_thesis: verum
end;
then A6: cot is_differentiable_on Z by A5, FDIFF_1:9;
 for x being Real st x in Z holds
((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) )
assume A7: x in Z ; ::_thesis: ((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))
then A8: sin . x <> 0 by A5, FDIFF_8:2;
A9: cos . x <> 0 by A3, A7, FDIFF_8:1;
((tan + cot) `| Z) . x = (diff (tan,x)) + (diff (cot,x)) by A1, A6, A4, A7, FDIFF_1:18
.= (1 / ((cos . x) ^2)) + (diff (cot,x)) by A9, FDIFF_7:46
.= (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) by A8, FDIFF_7:47 ;
hence  ((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ; ::_thesis: verum
end;
hence  ( tan + cot is_differentiable_on Z & ( for x being Real st x in Z holds
((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) ) by A1, A6, A4, FDIFF_1:18; ::_thesis: verum
end;

theorem :: FDIFF_10:7
for Z being open Subset of REAL holds
( sin * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( sin * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x) ) )
A1: for x being Real st x in Z holds
sin * sin is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sin * sin is_differentiable_in x )
assume  x in Z ; ::_thesis: sin * sin is_differentiable_in x
A2: sin is_differentiable_in sin . x by SIN_COS:64;
 sin is_differentiable_in x by SIN_COS:64;
hence  sin * sin is_differentiable_in x by A2, FDIFF_2:13; ::_thesis: verum
end;
 rng sin c= REAL ;
then A3: dom (sin * sin) = REAL by RELAT_1:27, SIN_COS:24;
then A4: sin * sin is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x)
proof
let x be Real; ::_thesis: ( x in Z implies ((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x) )
assume A5: x in Z ; ::_thesis: ((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x)
A6: sin is_differentiable_in sin . x by SIN_COS:64;
 sin is_differentiable_in x by SIN_COS:64;
then  diff ((sin * sin),x) = (diff (sin,(sin . x))) * (diff (sin,x)) by A6, FDIFF_2:13
.= (cos . (sin . x)) * (diff (sin,x)) by SIN_COS:64
.= (cos . (sin . x)) * (cos . x) by SIN_COS:64 ;
hence  ((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x) by A4, A5, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sin * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x) ) ) by A3, A1, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:8
for Z being open Subset of REAL holds
( sin * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( sin * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x)) ) )
A1: for x being Real st x in Z holds
sin * cos is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sin * cos is_differentiable_in x )
assume  x in Z ; ::_thesis: sin * cos is_differentiable_in x
A2: sin is_differentiable_in cos . x by SIN_COS:64;
 cos is_differentiable_in x by SIN_COS:63;
hence  sin * cos is_differentiable_in x by A2, FDIFF_2:13; ::_thesis: verum
end;
 rng cos c= dom cos by SIN_COS:24;
then A3: dom (sin * cos) = REAL by RELAT_1:27, SIN_COS:24;
then A4: sin * cos is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x))
proof
let x be Real; ::_thesis: ( x in Z implies ((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x)) )
assume A5: x in Z ; ::_thesis: ((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x))
A6: sin is_differentiable_in cos . x by SIN_COS:64;
 cos is_differentiable_in x by SIN_COS:63;
then  diff ((sin * cos),x) = (diff (sin,(cos . x))) * (diff (cos,x)) by A6, FDIFF_2:13
.= (cos . (cos . x)) * (diff (cos,x)) by SIN_COS:64
.= (cos . (cos . x)) * (- (sin . x)) by SIN_COS:63 ;
hence  ((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x)) by A4, A5, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sin * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x)) ) ) by A3, A1, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:9
for Z being open Subset of REAL holds
( cos * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( cos * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x)) ) )
A1: for x being Real st x in Z holds
cos * sin is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cos * sin is_differentiable_in x )
assume  x in Z ; ::_thesis: cos * sin is_differentiable_in x
A2: cos is_differentiable_in sin . x by SIN_COS:63;
 sin is_differentiable_in x by SIN_COS:64;
hence  cos * sin is_differentiable_in x by A2, FDIFF_2:13; ::_thesis: verum
end;
 rng sin c= dom sin by SIN_COS:24;
then A3: dom (cos * sin) = REAL by RELAT_1:27, SIN_COS:24;
then A4: cos * sin is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x))
proof
let x be Real; ::_thesis: ( x in Z implies ((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x)) )
assume A5: x in Z ; ::_thesis: ((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x))
A6: cos is_differentiable_in sin . x by SIN_COS:63;
 sin is_differentiable_in x by SIN_COS:64;
then  diff ((cos * sin),x) = (diff (cos,(sin . x))) * (diff (sin,x)) by A6, FDIFF_2:13
.= (- (sin . (sin . x))) * (diff (sin,x)) by SIN_COS:63
.= (- (sin . (sin . x))) * (cos . x) by SIN_COS:64 ;
hence  ((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x)) by A4, A5, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cos * sin is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x)) ) ) by A3, A1, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:10
for Z being open Subset of REAL holds
( cos * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( cos * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x) ) )
A1: for x being Real st x in Z holds
cos * cos is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cos * cos is_differentiable_in x )
assume  x in Z ; ::_thesis: cos * cos is_differentiable_in x
A2: cos is_differentiable_in cos . x by SIN_COS:63;
 cos is_differentiable_in x by SIN_COS:63;
hence  cos * cos is_differentiable_in x by A2, FDIFF_2:13; ::_thesis: verum
end;
 rng cos c= REAL ;
then A3: dom (cos * cos) = REAL by RELAT_1:27, SIN_COS:24;
then A4: cos * cos is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x)
proof
let x be Real; ::_thesis: ( x in Z implies ((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x) )
assume A5: x in Z ; ::_thesis: ((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x)
A6: cos is_differentiable_in cos . x by SIN_COS:63;
 cos is_differentiable_in x by SIN_COS:63;
then  diff ((cos * cos),x) = (diff (cos,(cos . x))) * (diff (cos,x)) by A6, FDIFF_2:13
.= (- (sin . (cos . x))) * (diff (cos,x)) by SIN_COS:63
.= (- (sin . (cos . x))) * (- (sin . x)) by SIN_COS:63 ;
hence  ((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x) by A4, A5, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cos * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x) ) ) by A3, A1, FDIFF_1:9; ::_thesis: verum
end;

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

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

theorem :: FDIFF_10:13
for Z being open Subset of REAL st Z c= dom (sin (#) cot) holds
( sin (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin (#) cot) implies ( sin (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) ) ) )
A1: for x being Real st x in Z holds
sin is_differentiable_in x by SIN_COS:64;
assume A2: Z c= dom (sin (#) cot) ; ::_thesis: ( sin (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) ) )
then A3: Z c= (dom sin) /\ (dom cot) by VALUED_1:def_4;
then A4: 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 A4, FDIFF_8:2;
hence  cot is_differentiable_in x by FDIFF_7:47; ::_thesis: verum
end;
then A5: cot is_differentiable_on Z by A4, FDIFF_1:9;
 Z c= dom sin by A3, XBOOLE_1:18;
then A6: sin is_differentiable_on Z by A1, FDIFF_1:9;
A7: for x being Real st x in Z holds
diff (cot,x) = - (1 / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies diff (cot,x) = - (1 / ((sin . x) ^2)) )
assume  x in Z ; ::_thesis: diff (cot,x) = - (1 / ((sin . x) ^2))
then  sin . x <> 0 by A4, FDIFF_8:2;
hence  diff (cot,x) = - (1 / ((sin . x) ^2)) by FDIFF_7:47; ::_thesis: verum
end;
 for x being Real st x in Z holds
((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x))
proof
let x be Real; ::_thesis: ( x in Z implies ((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) )
assume A8: x in Z ; ::_thesis: ((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x))
then ((sin (#) cot) `| Z) . x = ((diff (sin,x)) * (cot . x)) + ((sin . x) * (diff (cot,x))) by A2, A5, A6, FDIFF_1:21
.= ((cos . x) * (cot . x)) + ((sin . x) * (diff (cot,x))) by SIN_COS:64
.= ((cos . x) * (cot . x)) + ((sin . x) * (- (1 / ((sin . x) ^2)))) by A7, A8
.= ((cos . x) * (cot . x)) - ((sin . x) / ((sin . x) ^2))
.= ((cos . x) * (cot . x)) - (((sin . x) / (sin . x)) / (sin . x)) by XCMPLX_1:78
.= ((cos . x) * (cot . x)) - (1 / (sin . x)) by A4, A8, FDIFF_8:2, XCMPLX_1:60 ;
hence  ((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) ; ::_thesis: verum
end;
hence  ( sin (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) cot) `| Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:14
for Z being open Subset of REAL st Z c= dom (cos (#) tan) holds
( cos (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos (#) tan) implies ( cos (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) ) ) )
A1: for x being Real st x in Z holds
cos is_differentiable_in x by SIN_COS:63;
assume A2: Z c= dom (cos (#) tan) ; ::_thesis: ( cos (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) ) )
then A3: Z c= (dom cos) /\ (dom tan) by VALUED_1:def_4;
then A4: 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 A4, FDIFF_8:1;
hence  tan is_differentiable_in x by FDIFF_7:46; ::_thesis: verum
end;
then A5: tan is_differentiable_on Z by A4, FDIFF_1:9;
 Z c= dom cos by A3, XBOOLE_1:18;
then A6: cos is_differentiable_on Z by A1, FDIFF_1:9;
A7: for x being Real st x in Z holds
diff (tan,x) = 1 / ((cos . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies diff (tan,x) = 1 / ((cos . x) ^2) )
assume  x in Z ; ::_thesis: diff (tan,x) = 1 / ((cos . x) ^2)
then  cos . x <> 0 by A4, FDIFF_8:1;
hence  diff (tan,x) = 1 / ((cos . x) ^2) by FDIFF_7:46; ::_thesis: verum
end;
 for x being Real st x in Z holds
((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x))
proof
let x be Real; ::_thesis: ( x in Z implies ((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) )
assume A8: x in Z ; ::_thesis: ((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x))
then ((cos (#) tan) `| Z) . x = ((diff (cos,x)) * (tan . x)) + ((cos . x) * (diff (tan,x))) by A2, A5, A6, FDIFF_1:21
.= ((tan . x) * (- (sin . x))) + ((cos . x) * (diff (tan,x))) by SIN_COS:63
.= ((tan . x) * (- (sin . x))) + ((cos . x) * (1 / ((cos . x) ^2))) by A7, A8
.= (((sin . x) / (cos . x)) * (- ((sin . x) / 1))) + ((cos . x) / ((cos . x) ^2)) by A4, A8, RFUNCT_1:def_1
.= (- (((sin . x) ^2) / (cos . x))) + (((cos . x) / (cos . x)) / (cos . x)) by XCMPLX_1:78
.= (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) by A4, A8, FDIFF_8:1, XCMPLX_1:60 ;
hence  ((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) ; ::_thesis: verum
end;
hence  ( cos (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) tan) `| Z) . x = (- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:15
for Z being open Subset of REAL st Z c= dom (sin (#) cos) holds
( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin (#) cos) implies ( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2) ) ) )
A1: for x being Real st x in Z holds
sin is_differentiable_in x by SIN_COS:64;
A2: for x being Real st x in Z holds
cos is_differentiable_in x by SIN_COS:63;
assume A3: Z c= dom (sin (#) cos) ; ::_thesis: ( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2) ) )
then A4: Z c= (dom sin) /\ (dom cos) by VALUED_1:def_4;
then  Z c= dom cos by XBOOLE_1:18;
then A5: cos is_differentiable_on Z by A2, FDIFF_1:9;
 Z c= dom sin by A4, XBOOLE_1:18;
then A6: sin is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2) )
assume  x in Z ; ::_thesis: ((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2)
then ((sin (#) cos) `| Z) . x = ((diff (sin,x)) * (cos . x)) + ((sin . x) * (diff (cos,x))) by A3, A6, A5, FDIFF_1:21
.= ((cos . x) * (cos . x)) + ((sin . x) * (diff (cos,x))) by SIN_COS:64
.= ((cos . x) * (cos . x)) + ((sin . x) * (- (sin . x))) by SIN_COS:63
.= ((cos . x) ^2) - ((sin . x) ^2) ;
hence  ((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2) ; ::_thesis: verum
end;
hence  ( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) cos) `| Z) . x = ((cos . x) ^2) - ((sin . x) ^2) ) ) by A3, A6, A5, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:16
for Z being open Subset of REAL st Z c= dom (ln (#) sin) holds
( ln (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln (#) sin) implies ( ln (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) ) ) )
A1: for x being Real st x in Z holds
sin is_differentiable_in x by SIN_COS:64;
assume A2: Z c= dom (ln (#) sin) ; ::_thesis: ( ln (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) ) )
then A3: Z c= (dom ln) /\ (dom sin) by VALUED_1:def_4;
then  Z c= dom sin by XBOOLE_1:18;
then A4: sin is_differentiable_on Z by A1, FDIFF_1:9;
A5: Z c= dom ln by A3, XBOOLE_1:18;
A6: 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 A5, TAYLOR_1:18;
then  x in  {  g where g is Real : 0 < g  }  by XXREAL_1:230;
then  ex g being Real st
( x = g & 0 < g ) ;
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 A7: ln is_differentiable_on Z by A5, FDIFF_1:9;
A8: 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 A6;
then  x in  {  g where g is Real : 0 < g  }  ;
then  x in right_open_halfline 0 by XXREAL_1:230;
hence  diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum
end;
 for x being Real st x in Z holds
((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x))
proof
let x be Real; ::_thesis: ( x in Z implies ((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) )
assume A9: x in Z ; ::_thesis: ((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x))
then ((ln (#) sin) `| Z) . x = ((sin . x) * (diff (ln,x))) + ((ln . x) * (diff (sin,x))) by A2, A7, A4, FDIFF_1:21
.= ((sin . x) * (1 / x)) + ((ln . x) * (diff (sin,x))) by A8, A9
.= ((sin . x) / x) + ((ln . x) * (cos . x)) by SIN_COS:64 ;
hence  ((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) ; ::_thesis: verum
end;
hence  ( ln (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) sin) `| Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) ) ) by A2, A7, A4, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:17
for Z being open Subset of REAL st Z c= dom (ln (#) cos) holds
( ln (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln (#) cos) implies ( ln (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) ) ) )
A1: for x being Real st x in Z holds
cos is_differentiable_in x by SIN_COS:63;
assume A2: Z c= dom (ln (#) cos) ; ::_thesis: ( ln (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) ) )
then A3: Z c= (dom ln) /\ (dom cos) by VALUED_1:def_4;
then  Z c= dom cos by XBOOLE_1:18;
then A4: cos is_differentiable_on Z by A1, FDIFF_1:9;
A5: Z c= dom ln by A3, XBOOLE_1:18;
A6: 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 A5, TAYLOR_1:18;
then  x in  {  g where g is Real : 0 < g  }  by XXREAL_1:230;
then  ex g being Real st
( x = g & 0 < g ) ;
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 A7: ln is_differentiable_on Z by A5, FDIFF_1:9;
A8: 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 A6;
then  x in  {  g where g is Real : 0 < g  }  ;
then  x in right_open_halfline 0 by XXREAL_1:230;
hence  diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum
end;
 for x being Real st x in Z holds
((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x))
proof
let x be Real; ::_thesis: ( x in Z implies ((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) )
assume A9: x in Z ; ::_thesis: ((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x))
then ((ln (#) cos) `| Z) . x = ((cos . x) * (diff (ln,x))) + ((ln . x) * (diff (cos,x))) by A2, A7, A4, FDIFF_1:21
.= ((cos . x) * (1 / x)) + ((ln . x) * (diff (cos,x))) by A8, A9
.= ((cos . x) / x) + ((ln . x) * (- (sin . x))) by SIN_COS:63 ;
hence  ((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) ; ::_thesis: verum
end;
hence  ( ln (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) cos) `| Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) ) ) by A2, A7, A4, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:18
for Z being open Subset of REAL st Z c= dom (ln (#) exp_R) holds
( ln (#) exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln (#) exp_R) implies ( ln (#) exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x)) ) ) )
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 (ln (#) exp_R) ; ::_thesis: ( ln (#) exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x)) ) )
then A3: Z c= (dom ln) /\ (dom exp_R) by VALUED_1:def_4;
then  Z c= dom exp_R by XBOOLE_1:18;
then A4: exp_R is_differentiable_on Z by A1, FDIFF_1:9;
A5: Z c= dom ln by A3, XBOOLE_1:18;
A6: 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 A5, TAYLOR_1:18;
then  x in  {  g where g is Real : 0 < g  }  by XXREAL_1:230;
then  ex g being Real st
( x = g & 0 < g ) ;
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 A7: ln is_differentiable_on Z by A5, FDIFF_1:9;
A8: 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 A6;
then  x in  {  g where g is Real : 0 < g  }  ;
then  x in right_open_halfline 0 by XXREAL_1:230;
hence  diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum
end;
 for x being Real st x in Z holds
((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x))
proof
let x be Real; ::_thesis: ( x in Z implies ((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x)) )
assume A9: x in Z ; ::_thesis: ((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x))
then ((ln (#) exp_R) `| Z) . x = ((exp_R . x) * (diff (ln,x))) + ((ln . x) * (diff (exp_R,x))) by A2, A7, A4, FDIFF_1:21
.= ((exp_R . x) * (1 / x)) + ((ln . x) * (diff (exp_R,x))) by A8, A9
.= ((exp_R . x) * (1 / x)) + ((ln . x) * (exp_R . x)) by SIN_COS:65 ;
hence  ((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x)) ; ::_thesis: verum
end;
hence  ( ln (#) exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) exp_R) `| Z) . x = ((exp_R . x) / x) + ((ln . x) * (exp_R . x)) ) ) by A2, A7, A4, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:19
for Z being open Subset of REAL st Z c= dom (ln * ln) & ( for x being Real st x in Z holds
x > 0 ) holds
( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln * ln) & ( for x being Real st x in Z holds
x > 0 ) implies ( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) ) )
assume that
A1: Z c= dom (ln * ln) and
A2: for x being Real st x in Z holds
x > 0 ; ::_thesis: ( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) )
A3: for x being Real st x in Z holds
ln . x > 0
proof
let x be Real; ::_thesis: ( x in Z implies ln . x > 0 )
assume  x in Z ; ::_thesis: ln . x > 0
then A4: ln . x in right_open_halfline 0 by A1, FUNCT_1:11, TAYLOR_1:18;
 ].0,+infty.[ =  {  g where g is Real : 0 < g  }  by XXREAL_1:230;
then  ex g being Real st
( ln . x = g & 0 < g ) by A4;
hence  ln . x > 0 ; ::_thesis: verum
end;
A5: for x being Real st x in Z holds
ln * ln is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies ln * ln is_differentiable_in x )
assume A6: x in Z ; ::_thesis: ln * ln is_differentiable_in x
then A7: ln . x > 0 by A3;
 ln is_differentiable_in x by A2, A6, TAYLOR_1:18;
hence  ln * ln is_differentiable_in x by A7, TAYLOR_1:20; ::_thesis: verum
end;
then A8: ln * ln is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((ln * ln) `| Z) . x = 1 / ((ln . x) * x)
proof
let x be Real; ::_thesis: ( x in Z implies ((ln * ln) `| Z) . x = 1 / ((ln . x) * x) )
A9: ].0,+infty.[ =  {  g where g is Real : 0 < g  }  by XXREAL_1:230;
assume A10: x in Z ; ::_thesis: ((ln * ln) `| Z) . x = 1 / ((ln . x) * x)
then A11: ln . x > 0 by A3;
 x > 0 by A2, A10;
then A12: x in right_open_halfline 0 by A9;
 ln is_differentiable_in x by A2, A10, TAYLOR_1:18;
then  diff ((ln * ln),x) = (diff (ln,x)) / (ln . x) by A11, TAYLOR_1:20
.= (1 / (ln . x)) * (1 / x) by A12, TAYLOR_1:18
.= 1 / ((ln . x) * x) by XCMPLX_1:102 ;
hence  ((ln * ln) `| Z) . x = 1 / ((ln . x) * x) by A8, A10, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) ) by A1, A5, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:20
for Z being open Subset of REAL st Z c= dom (exp_R * exp_R) holds
( exp_R * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * exp_R) implies ( exp_R * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x) ) ) )
A1: for x being Real st x in Z holds
exp_R * exp_R is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies exp_R * exp_R is_differentiable_in x )
assume  x in Z ; ::_thesis: exp_R * exp_R is_differentiable_in x
A2: exp_R is_differentiable_in exp_R . x by SIN_COS:65;
 exp_R is_differentiable_in x by SIN_COS:65;
hence  exp_R * exp_R is_differentiable_in x by A2, FDIFF_2:13; ::_thesis: verum
end;
assume A3: Z c= dom (exp_R * exp_R) ; ::_thesis: ( exp_R * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x) ) )
then A4: exp_R * exp_R is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x)
proof
let x be Real; ::_thesis: ( x in Z implies ((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x) )
assume A5: x in Z ; ::_thesis: ((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x)
A6: exp_R is_differentiable_in exp_R . x by SIN_COS:65;
 exp_R is_differentiable_in x by SIN_COS:65;
then  diff ((exp_R * exp_R),x) = (diff (exp_R,(exp_R . x))) * (diff (exp_R,x)) by A6, FDIFF_2:13
.= (exp_R . (exp_R . x)) * (diff (exp_R,x)) by SIN_COS:65
.= (exp_R . (exp_R . x)) * (exp_R . x) by SIN_COS:65 ;
hence  ((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x) by A4, A5, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( exp_R * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * exp_R) `| Z) . x = (exp_R . (exp_R . x)) * (exp_R . x) ) ) by A3, A1, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:21
for Z being open Subset of REAL st Z c= dom (sin * tan) holds
( sin * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin * tan) implies ( sin * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2) ) ) )
assume A1: Z c= dom (sin * tan) ; ::_thesis: ( sin * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * tan) `| Z) . x = (cos (tan . 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 (sin / cos) by A1, FUNCT_1:11;
hence  cos . x <> 0 by FDIFF_8:1; ::_thesis: verum
end;
A3: for x being Real st x in Z holds
sin * tan is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sin * tan is_differentiable_in x )
assume  x in Z ; ::_thesis: sin * tan is_differentiable_in x
then  cos . x <> 0 by A2;
then A4: tan is_differentiable_in x by FDIFF_7:46;
 sin is_differentiable_in tan . x by SIN_COS:64;
hence  sin * tan is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum
end;
then A5: sin * tan is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2) )
A6: sin is_differentiable_in tan . x by SIN_COS:64;
assume A7: x in Z ; ::_thesis: ((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2)
then A8: cos . x <> 0 by A2;
then  tan is_differentiable_in x by FDIFF_7:46;
then  diff ((sin * tan),x) = (diff (sin,(tan . x))) * (diff (tan,x)) by A6, FDIFF_2:13
.= (cos (tan . x)) * (diff (tan,x)) by SIN_COS:64
.= (cos (tan . x)) * (1 / ((cos . x) ^2)) by A8, FDIFF_7:46
.= (cos (tan . x)) / ((cos . x) ^2) ;
hence  ((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2) by A5, A7, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sin * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * tan) `| Z) . x = (cos (tan . x)) / ((cos . x) ^2) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:22
for Z being open Subset of REAL st Z c= dom (sin * cot) holds
( sin * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin * cot) implies ( sin * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2)) ) ) )
assume A1: Z c= dom (sin * cot) ; ::_thesis: ( sin * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * cot) `| Z) . x = - ((cos (cot . 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 (cos / sin) by A1, FUNCT_1:11;
hence  sin . x <> 0 by FDIFF_8:2; ::_thesis: verum
end;
A3: for x being Real st x in Z holds
sin * cot is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sin * cot is_differentiable_in x )
assume  x in Z ; ::_thesis: sin * cot is_differentiable_in x
then  sin . x <> 0 by A2;
then A4: cot is_differentiable_in x by FDIFF_7:47;
 sin is_differentiable_in cot . x by SIN_COS:64;
hence  sin * cot is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum
end;
then A5: sin * cot is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2)) )
A6: sin is_differentiable_in cot . x by SIN_COS:64;
assume A7: x in Z ; ::_thesis: ((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2))
then A8: sin . x <> 0 by A2;
then  cot is_differentiable_in x by FDIFF_7:47;
then  diff ((sin * cot),x) = (diff (sin,(cot . x))) * (diff (cot,x)) by A6, FDIFF_2:13
.= (cos (cot . x)) * (diff (cot,x)) by SIN_COS:64
.= (cos (cot . x)) * (- (1 / ((sin . x) ^2))) by A8, FDIFF_7:47
.= - ((cos (cot . x)) / ((sin . x) ^2)) ;
hence  ((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2)) by A5, A7, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sin * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * cot) `| Z) . x = - ((cos (cot . x)) / ((sin . x) ^2)) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:23
for Z being open Subset of REAL st Z c= dom (cos * tan) holds
( cos * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos * tan) implies ( cos * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2)) ) ) )
assume A1: Z c= dom (cos * tan) ; ::_thesis: ( cos * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * tan) `| Z) . x = - ((sin (tan . 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 (sin / cos) by A1, FUNCT_1:11;
hence  cos . x <> 0 by FDIFF_8:1; ::_thesis: verum
end;
A3: for x being Real st x in Z holds
cos * tan is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cos * tan is_differentiable_in x )
assume  x in Z ; ::_thesis: cos * tan is_differentiable_in x
then  cos . x <> 0 by A2;
then A4: tan is_differentiable_in x by FDIFF_7:46;
 cos is_differentiable_in tan . x by SIN_COS:63;
hence  cos * tan is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum
end;
then A5: cos * tan is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2)) )
A6: cos is_differentiable_in tan . x by SIN_COS:63;
assume A7: x in Z ; ::_thesis: ((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2))
then A8: cos . x <> 0 by A2;
then  tan is_differentiable_in x by FDIFF_7:46;
then  diff ((cos * tan),x) = (diff (cos,(tan . x))) * (diff (tan,x)) by A6, FDIFF_2:13
.= (- (sin (tan . x))) * (diff (tan,x)) by SIN_COS:63
.= (- (sin (tan . x))) * (1 / ((cos . x) ^2)) by A8, FDIFF_7:46
.= - ((sin (tan . x)) / ((cos . x) ^2)) ;
hence  ((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2)) by A5, A7, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cos * tan is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * tan) `| Z) . x = - ((sin (tan . x)) / ((cos . x) ^2)) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:24
for Z being open Subset of REAL st Z c= dom (cos * cot) holds
( cos * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos * cot) implies ( cos * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2) ) ) )
assume A1: Z c= dom (cos * cot) ; ::_thesis: ( cos * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * cot) `| Z) . x = (sin (cot . 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 (cos / sin) by A1, FUNCT_1:11;
hence  sin . x <> 0 by FDIFF_8:2; ::_thesis: verum
end;
A3: for x being Real st x in Z holds
cos * cot is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cos * cot is_differentiable_in x )
assume  x in Z ; ::_thesis: cos * cot is_differentiable_in x
then  sin . x <> 0 by A2;
then A4: cot is_differentiable_in x by FDIFF_7:47;
 cos is_differentiable_in cot . x by SIN_COS:63;
hence  cos * cot is_differentiable_in x by A4, FDIFF_2:13; ::_thesis: verum
end;
then A5: cos * cot is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2) )
A6: cos is_differentiable_in cot . x by SIN_COS:63;
assume A7: x in Z ; ::_thesis: ((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2)
then A8: sin . x <> 0 by A2;
then  cot is_differentiable_in x by FDIFF_7:47;
then  diff ((cos * cot),x) = (diff (cos,(cot . x))) * (diff (cot,x)) by A6, FDIFF_2:13
.= (- (sin (cot . x))) * (diff (cot,x)) by SIN_COS:63
.= (- (sin (cot . x))) * (- (1 / ((sin . x) ^2))) by A8, FDIFF_7:47
.= (sin (cot . x)) / ((sin . x) ^2) ;
hence  ((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2) by A5, A7, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cos * cot is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * cot) `| Z) . x = (sin (cot . x)) / ((sin . x) ^2) ) ) by A1, A3, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:25
for Z being open Subset of REAL st Z c= dom (sin (#) (tan + cot)) holds
( sin (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin (#) (tan + cot)) implies ( sin (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) )
A1: for x being Real st x in Z holds
sin is_differentiable_in x by SIN_COS:64;
assume A2: Z c= dom (sin (#) (tan + cot)) ; ::_thesis: ( sin (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) )
then A3: Z c= (dom (tan + cot)) /\ (dom sin) by VALUED_1:def_4;
then A4: Z c= dom (tan + cot) by XBOOLE_1:18;
then A5: tan + cot is_differentiable_on Z by Th6;
 Z c= dom sin by A3, XBOOLE_1:18;
then A6: sin is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))))
proof
let x be Real; ::_thesis: ( x in Z implies ((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) )
assume A7: x in Z ; ::_thesis: ((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))))
then ((sin (#) (tan + cot)) `| Z) . x = (((tan + cot) . x) * (diff (sin,x))) + ((sin . x) * (diff ((tan + cot),x))) by A2, A5, A6, FDIFF_1:21
.= (((tan . x) + (cot . x)) * (diff (sin,x))) + ((sin . x) * (diff ((tan + cot),x))) by A4, A7, VALUED_1:def_1
.= (((tan . x) + (cot . x)) * (cos . x)) + ((sin . x) * (diff ((tan + cot),x))) by SIN_COS:64
.= (((tan . x) + (cot . x)) * (cos . x)) + ((sin . x) * (((tan + cot) `| Z) . x)) by A5, A7, FDIFF_1:def_7
.= (((tan . x) + (cot . x)) * (cos . x)) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) by A4, A7, Th6 ;
hence  ((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ; ::_thesis: verum
end;
hence  ( sin (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (tan + cot)) `| Z) . x = ((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:26
for Z being open Subset of REAL st Z c= dom (cos (#) (tan + cot)) holds
( cos (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos (#) (tan + cot)) implies ( cos (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) )
A1: for x being Real st x in Z holds
cos is_differentiable_in x by SIN_COS:63;
assume A2: Z c= dom (cos (#) (tan + cot)) ; ::_thesis: ( cos (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) )
then A3: Z c= (dom (tan + cot)) /\ (dom cos) by VALUED_1:def_4;
then A4: Z c= dom (tan + cot) by XBOOLE_1:18;
then A5: tan + cot is_differentiable_on Z by Th6;
 Z c= dom cos by A3, XBOOLE_1:18;
then A6: cos is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))))
proof
let x be Real; ::_thesis: ( x in Z implies ((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) )
assume A7: x in Z ; ::_thesis: ((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))))
then ((cos (#) (tan + cot)) `| Z) . x = (((tan + cot) . x) * (diff (cos,x))) + ((cos . x) * (diff ((tan + cot),x))) by A2, A5, A6, FDIFF_1:21
.= (((tan . x) + (cot . x)) * (diff (cos,x))) + ((cos . x) * (diff ((tan + cot),x))) by A4, A7, VALUED_1:def_1
.= (((tan . x) + (cot . x)) * (- (sin . x))) + ((cos . x) * (diff ((tan + cot),x))) by SIN_COS:63
.= (((tan . x) + (cot . x)) * (- (sin . x))) + ((cos . x) * (((tan + cot) `| Z) . x)) by A5, A7, FDIFF_1:def_7
.= (((tan . x) + (cot . x)) * (- (sin . x))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) by A4, A7, Th6 ;
hence  ((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ; ::_thesis: verum
end;
hence  ( cos (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (tan + cot)) `| Z) . x = (- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:27
for Z being open Subset of REAL st Z c= dom (sin (#) (tan - cot)) holds
( sin (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin (#) (tan - cot)) implies ( sin (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) )
A1: for x being Real st x in Z holds
sin is_differentiable_in x by SIN_COS:64;
assume A2: Z c= dom (sin (#) (tan - cot)) ; ::_thesis: ( sin (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) )
then A3: Z c= (dom (tan - cot)) /\ (dom sin) by VALUED_1:def_4;
then A4: Z c= dom (tan - cot) by XBOOLE_1:18;
then A5: tan - cot is_differentiable_on Z by Th5;
 Z c= dom sin by A3, XBOOLE_1:18;
then A6: sin is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))))
proof
let x be Real; ::_thesis: ( x in Z implies ((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) )
assume A7: x in Z ; ::_thesis: ((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))))
then ((sin (#) (tan - cot)) `| Z) . x = (((tan - cot) . x) * (diff (sin,x))) + ((sin . x) * (diff ((tan - cot),x))) by A2, A5, A6, FDIFF_1:21
.= (((tan . x) - (cot . x)) * (diff (sin,x))) + ((sin . x) * (diff ((tan - cot),x))) by A4, A7, VALUED_1:13
.= (((tan . x) - (cot . x)) * (cos . x)) + ((sin . x) * (diff ((tan - cot),x))) by SIN_COS:64
.= (((tan . x) - (cot . x)) * (cos . x)) + ((sin . x) * (((tan - cot) `| Z) . x)) by A5, A7, FDIFF_1:def_7
.= (((tan . x) - (cot . x)) * (cos . x)) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) by A4, A7, Th5 ;
hence  ((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ; ::_thesis: verum
end;
hence  ( sin (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (tan - cot)) `| Z) . x = ((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:28
for Z being open Subset of REAL st Z c= dom (cos (#) (tan - cot)) holds
( cos (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos (#) (tan - cot)) implies ( cos (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) )
A1: for x being Real st x in Z holds
cos is_differentiable_in x by SIN_COS:63;
assume A2: Z c= dom (cos (#) (tan - cot)) ; ::_thesis: ( cos (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) )
then A3: Z c= (dom (tan - cot)) /\ (dom cos) by VALUED_1:def_4;
then A4: Z c= dom (tan - cot) by XBOOLE_1:18;
then A5: tan - cot is_differentiable_on Z by Th5;
 Z c= dom cos by A3, XBOOLE_1:18;
then A6: cos is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))))
proof
let x be Real; ::_thesis: ( x in Z implies ((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) )
assume A7: x in Z ; ::_thesis: ((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))))
then ((cos (#) (tan - cot)) `| Z) . x = (((tan - cot) . x) * (diff (cos,x))) + ((cos . x) * (diff ((tan - cot),x))) by A2, A5, A6, FDIFF_1:21
.= (((tan . x) - (cot . x)) * (diff (cos,x))) + ((cos . x) * (diff ((tan - cot),x))) by A4, A7, VALUED_1:13
.= (((tan . x) - (cot . x)) * (- (sin . x))) + ((cos . x) * (diff ((tan - cot),x))) by SIN_COS:63
.= (((tan . x) - (cot . x)) * (- (sin . x))) + ((cos . x) * (((tan - cot) `| Z) . x)) by A5, A7, FDIFF_1:def_7
.= (((tan . x) - (cot . x)) * (- (sin . x))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) by A4, A7, Th5 ;
hence  ((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ; ::_thesis: verum
end;
hence  ( cos (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (tan - cot)) `| Z) . x = (- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:29
for Z being open Subset of REAL st Z c= dom (exp_R (#) (tan + cot)) holds
( exp_R (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R (#) (tan + cot)) implies ( exp_R (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) )
assume A1: Z c= dom (exp_R (#) (tan + cot)) ; ::_thesis: ( exp_R (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) )
then  Z c= (dom (tan + cot)) /\ (dom exp_R) by VALUED_1:def_4;
then A2: Z c= dom (tan + cot) by XBOOLE_1:18;
then A3: tan + cot is_differentiable_on Z by Th6;
A4: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16;
 for x being Real st x in Z holds
((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))))
proof
let x be Real; ::_thesis: ( x in Z implies ((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) )
assume A5: x in Z ; ::_thesis: ((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))))
then ((exp_R (#) (tan + cot)) `| Z) . x = (((tan + cot) . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((tan + cot),x))) by A1, A3, A4, FDIFF_1:21
.= (((tan . x) + (cot . x)) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((tan + cot),x))) by A2, A5, VALUED_1:def_1
.= ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * (diff ((tan + cot),x))) by TAYLOR_1:16
.= ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * (((tan + cot) `| Z) . x)) by A3, A5, FDIFF_1:def_7
.= ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) by A2, A5, Th6 ;
hence  ((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ; ::_thesis: verum
end;
hence  ( exp_R (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) by A1, A3, A4, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:30
for Z being open Subset of REAL st Z c= dom (exp_R (#) (tan - cot)) holds
( exp_R (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R (#) (tan - cot)) implies ( exp_R (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) )
assume A1: Z c= dom (exp_R (#) (tan - cot)) ; ::_thesis: ( exp_R (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) )
then  Z c= (dom (tan - cot)) /\ (dom exp_R) by VALUED_1:def_4;
then A2: Z c= dom (tan - cot) by XBOOLE_1:18;
then A3: tan - cot is_differentiable_on Z by Th5;
A4: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16;
 for x being Real st x in Z holds
((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))))
proof
let x be Real; ::_thesis: ( x in Z implies ((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) )
assume A5: x in Z ; ::_thesis: ((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))))
then ((exp_R (#) (tan - cot)) `| Z) . x = (((tan - cot) . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((tan - cot),x))) by A1, A3, A4, FDIFF_1:21
.= (((tan . x) - (cot . x)) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((tan - cot),x))) by A2, A5, VALUED_1:13
.= ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * (diff ((tan - cot),x))) by TAYLOR_1:16
.= ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * (((tan - cot) `| Z) . x)) by A3, A5, FDIFF_1:def_7
.= ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) by A2, A5, Th5 ;
hence  ((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ; ::_thesis: verum
end;
hence  ( exp_R (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) by A1, A3, A4, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:31
for Z being open Subset of REAL st Z c= dom (sin (#) (sin + cos)) holds
( sin (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin (#) (sin + cos)) implies ( sin (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) )
A1: for x being Real st x in Z holds
sin is_differentiable_in x by SIN_COS:64;
assume A2: Z c= dom (sin (#) (sin + cos)) ; ::_thesis: ( sin (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) )
then A3: Z c= (dom (sin + cos)) /\ (dom sin) by VALUED_1:def_4;
then A4: Z c= dom (sin + cos) by XBOOLE_1:18;
then A5: sin + cos is_differentiable_on Z by FDIFF_7:38;
 Z c= dom sin by A3, XBOOLE_1:18;
then A6: sin is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) )
assume A7: x in Z ; ::_thesis: ((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2)
then ((sin (#) (sin + cos)) `| Z) . x = (((sin + cos) . x) * (diff (sin,x))) + ((sin . x) * (diff ((sin + cos),x))) by A2, A5, A6, FDIFF_1:21
.= (((sin . x) + (cos . x)) * (diff (sin,x))) + ((sin . x) * (diff ((sin + cos),x))) by VALUED_1:1
.= (((sin . x) + (cos . x)) * (cos . x)) + ((sin . x) * (diff ((sin + cos),x))) by SIN_COS:64
.= (((sin . x) + (cos . x)) * (cos . x)) + ((sin . x) * (((sin + cos) `| Z) . x)) by A5, A7, FDIFF_1:def_7
.= (((sin . x) + (cos . x)) * (cos . x)) + ((sin . x) * ((cos . x) - (sin . x))) by A4, A7, FDIFF_7:38 ;
hence  ((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ; ::_thesis: verum
end;
hence  ( sin (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:32
for Z being open Subset of REAL st Z c= dom (sin (#) (sin - cos)) holds
( sin (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin (#) (sin - cos)) implies ( sin (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) ) ) )
A1: for x being Real st x in Z holds
sin is_differentiable_in x by SIN_COS:64;
assume A2: Z c= dom (sin (#) (sin - cos)) ; ::_thesis: ( sin (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) ) )
then A3: Z c= (dom (sin - cos)) /\ (dom sin) by VALUED_1:def_4;
then A4: Z c= dom (sin - cos) by XBOOLE_1:18;
then A5: sin - cos is_differentiable_on Z by FDIFF_7:39;
 Z c= dom sin by A3, XBOOLE_1:18;
then A6: sin is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) )
assume A7: x in Z ; ::_thesis: ((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2)
then ((sin (#) (sin - cos)) `| Z) . x = (((sin - cos) . x) * (diff (sin,x))) + ((sin . x) * (diff ((sin - cos),x))) by A2, A5, A6, FDIFF_1:21
.= (((sin . x) - (cos . x)) * (diff (sin,x))) + ((sin . x) * (diff ((sin - cos),x))) by A4, A7, VALUED_1:13
.= (((sin . x) - (cos . x)) * (cos . x)) + ((sin . x) * (diff ((sin - cos),x))) by SIN_COS:64
.= (((sin . x) - (cos . x)) * (cos . x)) + ((sin . x) * (((sin - cos) `| Z) . x)) by A5, A7, FDIFF_1:def_7
.= (((sin . x) - (cos . x)) * (cos . x)) + ((sin . x) * ((cos . x) + (sin . x))) by A4, A7, FDIFF_7:39 ;
hence  ((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) ; ::_thesis: verum
end;
hence  ( sin (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (sin - cos)) `| Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:33
for Z being open Subset of REAL st Z c= dom (cos (#) (sin - cos)) holds
( cos (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos (#) (sin - cos)) implies ( cos (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) )
A1: for x being Real st x in Z holds
cos is_differentiable_in x by SIN_COS:63;
assume A2: Z c= dom (cos (#) (sin - cos)) ; ::_thesis: ( cos (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) )
then A3: Z c= (dom (sin - cos)) /\ (dom cos) by VALUED_1:def_4;
then A4: Z c= dom (sin - cos) by XBOOLE_1:18;
then A5: sin - cos is_differentiable_on Z by FDIFF_7:39;
 Z c= dom cos by A3, XBOOLE_1:18;
then A6: cos is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) )
assume A7: x in Z ; ::_thesis: ((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2)
then ((cos (#) (sin - cos)) `| Z) . x = (((sin - cos) . x) * (diff (cos,x))) + ((cos . x) * (diff ((sin - cos),x))) by A2, A5, A6, FDIFF_1:21
.= (((sin . x) - (cos . x)) * (diff (cos,x))) + ((cos . x) * (diff ((sin - cos),x))) by A4, A7, VALUED_1:13
.= (((sin . x) - (cos . x)) * (- (sin . x))) + ((cos . x) * (diff ((sin - cos),x))) by SIN_COS:63
.= (((sin . x) - (cos . x)) * (- (sin . x))) + ((cos . x) * (((sin - cos) `| Z) . x)) by A5, A7, FDIFF_1:def_7
.= (((sin . x) - (cos . x)) * (- (sin . x))) + ((cos . x) * ((cos . x) + (sin . x))) by A4, A7, FDIFF_7:39 ;
hence  ((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ; ::_thesis: verum
end;
hence  ( cos (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (sin - cos)) `| Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:34
for Z being open Subset of REAL st Z c= dom (cos (#) (sin + cos)) holds
( cos (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos (#) (sin + cos)) implies ( cos (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) )
A1: for x being Real st x in Z holds
cos is_differentiable_in x by SIN_COS:63;
assume A2: Z c= dom (cos (#) (sin + cos)) ; ::_thesis: ( cos (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) )
then A3: Z c= (dom (sin + cos)) /\ (dom cos) by VALUED_1:def_4;
then A4: Z c= dom (sin + cos) by XBOOLE_1:18;
then A5: sin + cos is_differentiable_on Z by FDIFF_7:38;
 Z c= dom cos by A3, XBOOLE_1:18;
then A6: cos is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) )
assume A7: x in Z ; ::_thesis: ((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2)
then ((cos (#) (sin + cos)) `| Z) . x = (((sin + cos) . x) * (diff (cos,x))) + ((cos . x) * (diff ((sin + cos),x))) by A2, A5, A6, FDIFF_1:21
.= (((sin . x) + (cos . x)) * (diff (cos,x))) + ((cos . x) * (diff ((sin + cos),x))) by VALUED_1:1
.= (((sin . x) + (cos . x)) * (- (sin . x))) + ((cos . x) * (diff ((sin + cos),x))) by SIN_COS:63
.= (((sin . x) + (cos . x)) * (- (sin . x))) + ((cos . x) * (((sin + cos) `| Z) . x)) by A5, A7, FDIFF_1:def_7
.= (((sin . x) + (cos . x)) * (- (sin . x))) + ((cos . x) * ((cos . x) - (sin . x))) by A4, A7, FDIFF_7:38 ;
hence  ((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ; ::_thesis: verum
end;
hence  ( cos (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (sin + cos)) `| Z) . x = (((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) ) by A2, A5, A6, FDIFF_1:21; ::_thesis: verum
end;

theorem :: FDIFF_10:35
for Z being open Subset of REAL st Z c= dom (sin * (tan + cot)) holds
( sin * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin * (tan + cot)) implies ( sin * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) ) )
assume A1: Z c= dom (sin * (tan + cot)) ; ::_thesis: ( sin * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) )
 dom (sin * (tan + cot)) c= dom (tan + cot) by RELAT_1:25;
then A2: Z c= dom (tan + cot) by A1, XBOOLE_1:1;
then A3: tan + cot is_differentiable_on Z by Th6;
A4: for x being Real st x in Z holds
sin * (tan + cot) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sin * (tan + cot) is_differentiable_in x )
assume  x in Z ; ::_thesis: sin * (tan + cot) is_differentiable_in x
then A5: tan + cot is_differentiable_in x by A3, FDIFF_1:9;
 sin is_differentiable_in (tan + cot) . x by SIN_COS:64;
hence  sin * (tan + cot) is_differentiable_in x by A5, FDIFF_2:13; ::_thesis: verum
end;
then A6: sin * (tan + cot) is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies ((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) )
A7: sin is_differentiable_in (tan + cot) . x by SIN_COS:64;
assume A8: x in Z ; ::_thesis: ((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))
then  tan + cot is_differentiable_in x by A3, FDIFF_1:9;
then  diff ((sin * (tan + cot)),x) = (diff (sin,((tan + cot) . x))) * (diff ((tan + cot),x)) by A7, FDIFF_2:13
.= (cos . ((tan + cot) . x)) * (diff ((tan + cot),x)) by SIN_COS:64
.= (cos . ((tan + cot) . x)) * (((tan + cot) `| Z) . x) by A3, A8, FDIFF_1:def_7
.= (cos . ((tan + cot) . x)) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A2, A8, Th6
.= (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A2, A8, VALUED_1:def_1 ;
hence  ((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A6, A8, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sin * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * (tan + cot)) `| Z) . x = (cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:36
for Z being open Subset of REAL st Z c= dom (sin * (tan - cot)) holds
( sin * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin * (tan - cot)) implies ( sin * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) ) )
assume A1: Z c= dom (sin * (tan - cot)) ; ::_thesis: ( sin * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) )
 dom (sin * (tan - cot)) c= dom (tan - cot) by RELAT_1:25;
then A2: Z c= dom (tan - cot) by A1, XBOOLE_1:1;
then A3: tan - cot is_differentiable_on Z by Th5;
A4: for x being Real st x in Z holds
sin * (tan - cot) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies sin * (tan - cot) is_differentiable_in x )
assume  x in Z ; ::_thesis: sin * (tan - cot) is_differentiable_in x
then A5: tan - cot is_differentiable_in x by A3, FDIFF_1:9;
 sin is_differentiable_in (tan - cot) . x by SIN_COS:64;
hence  sin * (tan - cot) is_differentiable_in x by A5, FDIFF_2:13; ::_thesis: verum
end;
then A6: sin * (tan - cot) is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies ((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) )
A7: sin is_differentiable_in (tan - cot) . x by SIN_COS:64;
assume A8: x in Z ; ::_thesis: ((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))
then  tan - cot is_differentiable_in x by A3, FDIFF_1:9;
then  diff ((sin * (tan - cot)),x) = (diff (sin,((tan - cot) . x))) * (diff ((tan - cot),x)) by A7, FDIFF_2:13
.= (cos . ((tan - cot) . x)) * (diff ((tan - cot),x)) by SIN_COS:64
.= (cos . ((tan - cot) . x)) * (((tan - cot) `| Z) . x) by A3, A8, FDIFF_1:def_7
.= (cos . ((tan - cot) . x)) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A2, A8, Th5
.= (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A2, A8, VALUED_1:13 ;
hence  ((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A6, A8, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( sin * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * (tan - cot)) `| Z) . x = (cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:37
for Z being open Subset of REAL st Z c= dom (cos * (tan - cot)) holds
( cos * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos * (tan - cot)) implies ( cos * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) )
assume A1: Z c= dom (cos * (tan - cot)) ; ::_thesis: ( cos * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) )
 dom (cos * (tan - cot)) c= dom (tan - cot) by RELAT_1:25;
then A2: Z c= dom (tan - cot) by A1, XBOOLE_1:1;
then A3: tan - cot is_differentiable_on Z by Th5;
A4: for x being Real st x in Z holds
cos * (tan - cot) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cos * (tan - cot) is_differentiable_in x )
assume  x in Z ; ::_thesis: cos * (tan - cot) is_differentiable_in x
then A5: tan - cot is_differentiable_in x by A3, FDIFF_1:9;
 cos is_differentiable_in (tan - cot) . x by SIN_COS:63;
hence  cos * (tan - cot) is_differentiable_in x by A5, FDIFF_2:13; ::_thesis: verum
end;
then A6: cos * (tan - cot) is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))))
proof
let x be Real; ::_thesis: ( x in Z implies ((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) )
A7: cos is_differentiable_in (tan - cot) . x by SIN_COS:63;
assume A8: x in Z ; ::_thesis: ((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))))
then  tan - cot is_differentiable_in x by A3, FDIFF_1:9;
then  diff ((cos * (tan - cot)),x) = (diff (cos,((tan - cot) . x))) * (diff ((tan - cot),x)) by A7, FDIFF_2:13
.= (- (sin . ((tan - cot) . x))) * (diff ((tan - cot),x)) by SIN_COS:63
.= (- (sin . ((tan - cot) . x))) * (((tan - cot) `| Z) . x) by A3, A8, FDIFF_1:def_7
.= (- (sin . ((tan - cot) . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A2, A8, Th5
.= (- (sin . ((tan . x) - (cot . x)))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A2, A8, VALUED_1:13 ;
hence  ((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) by A6, A8, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cos * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * (tan - cot)) `| Z) . x = - ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:38
for Z being open Subset of REAL st Z c= dom (cos * (tan + cot)) holds
( cos * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos * (tan + cot)) implies ( cos * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) )
assume A1: Z c= dom (cos * (tan + cot)) ; ::_thesis: ( cos * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) )
 dom (cos * (tan + cot)) c= dom (tan + cot) by RELAT_1:25;
then A2: Z c= dom (tan + cot) by A1, XBOOLE_1:1;
then A3: tan + cot is_differentiable_on Z by Th6;
A4: for x being Real st x in Z holds
cos * (tan + cot) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies cos * (tan + cot) is_differentiable_in x )
assume  x in Z ; ::_thesis: cos * (tan + cot) is_differentiable_in x
then A5: tan + cot is_differentiable_in x by A3, FDIFF_1:9;
 cos is_differentiable_in (tan + cot) . x by SIN_COS:63;
hence  cos * (tan + cot) is_differentiable_in x by A5, FDIFF_2:13; ::_thesis: verum
end;
then A6: cos * (tan + cot) is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))))
proof
let x be Real; ::_thesis: ( x in Z implies ((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) )
A7: cos is_differentiable_in (tan + cot) . x by SIN_COS:63;
assume A8: x in Z ; ::_thesis: ((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))))
then  tan + cot is_differentiable_in x by A3, FDIFF_1:9;
then  diff ((cos * (tan + cot)),x) = (diff (cos,((tan + cot) . x))) * (diff ((tan + cot),x)) by A7, FDIFF_2:13
.= (- (sin . ((tan + cot) . x))) * (diff ((tan + cot),x)) by SIN_COS:63
.= (- (sin . ((tan + cot) . x))) * (((tan + cot) `| Z) . x) by A3, A8, FDIFF_1:def_7
.= (- (sin . ((tan + cot) . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A2, A8, Th6
.= (- (sin . ((tan . x) + (cot . x)))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A2, A8, VALUED_1:def_1 ;
hence  ((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) by A6, A8, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( cos * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * (tan + cot)) `| Z) . x = - ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:39
for Z being open Subset of REAL st Z c= dom (exp_R * (tan + cot)) holds
( exp_R * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * (tan + cot)) implies ( exp_R * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) ) )
assume A1: Z c= dom (exp_R * (tan + cot)) ; ::_thesis: ( exp_R * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) )
 dom (exp_R * (tan + cot)) c= dom (tan + cot) by RELAT_1:25;
then A2: Z c= dom (tan + cot) by A1, XBOOLE_1:1;
then A3: tan + cot is_differentiable_on Z by Th6;
A4: for x being Real st x in Z holds
exp_R * (tan + cot) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies exp_R * (tan + cot) is_differentiable_in x )
assume  x in Z ; ::_thesis: exp_R * (tan + cot) is_differentiable_in x
then A5: tan + cot is_differentiable_in x by A3, FDIFF_1:9;
 exp_R is_differentiable_in (tan + cot) . x by SIN_COS:65;
hence  exp_R * (tan + cot) is_differentiable_in x by A5, FDIFF_2:13; ::_thesis: verum
end;
then A6: exp_R * (tan + cot) is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies ((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) )
A7: exp_R is_differentiable_in (tan + cot) . x by SIN_COS:65;
assume A8: x in Z ; ::_thesis: ((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))
then  tan + cot is_differentiable_in x by A3, FDIFF_1:9;
then  diff ((exp_R * (tan + cot)),x) = (diff (exp_R,((tan + cot) . x))) * (diff ((tan + cot),x)) by A7, FDIFF_2:13
.= (exp_R . ((tan + cot) . x)) * (diff ((tan + cot),x)) by SIN_COS:65
.= (exp_R . ((tan + cot) . x)) * (((tan + cot) `| Z) . x) by A3, A8, FDIFF_1:def_7
.= (exp_R . ((tan + cot) . x)) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A2, A8, Th6
.= (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A2, A8, VALUED_1:def_1 ;
hence  ((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) by A6, A8, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( exp_R * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:40
for Z being open Subset of REAL st Z c= dom (exp_R * (tan - cot)) holds
( exp_R * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * (tan - cot)) implies ( exp_R * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) ) )
assume A1: Z c= dom (exp_R * (tan - cot)) ; ::_thesis: ( exp_R * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) )
 dom (exp_R * (tan - cot)) c= dom (tan - cot) by RELAT_1:25;
then A2: Z c= dom (tan - cot) by A1, XBOOLE_1:1;
then A3: tan - cot is_differentiable_on Z by Th5;
A4: for x being Real st x in Z holds
exp_R * (tan - cot) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in Z implies exp_R * (tan - cot) is_differentiable_in x )
assume  x in Z ; ::_thesis: exp_R * (tan - cot) is_differentiable_in x
then A5: tan - cot is_differentiable_in x by A3, FDIFF_1:9;
 exp_R is_differentiable_in (tan - cot) . x by SIN_COS:65;
hence  exp_R * (tan - cot) is_differentiable_in x by A5, FDIFF_2:13; ::_thesis: verum
end;
then A6: exp_R * (tan - cot) is_differentiable_on Z by A1, FDIFF_1:9;
 for x being Real st x in Z holds
((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies ((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) )
A7: exp_R is_differentiable_in (tan - cot) . x by SIN_COS:65;
assume A8: x in Z ; ::_thesis: ((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))
then  tan - cot is_differentiable_in x by A3, FDIFF_1:9;
then  diff ((exp_R * (tan - cot)),x) = (diff (exp_R,((tan - cot) . x))) * (diff ((tan - cot),x)) by A7, FDIFF_2:13
.= (exp_R . ((tan - cot) . x)) * (diff ((tan - cot),x)) by SIN_COS:65
.= (exp_R . ((tan - cot) . x)) * (((tan - cot) `| Z) . x) by A3, A8, FDIFF_1:def_7
.= (exp_R . ((tan - cot) . x)) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A2, A8, Th5
.= (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A2, A8, VALUED_1:13 ;
hence  ((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) by A6, A8, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( exp_R * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum
end;

theorem :: FDIFF_10:41
for Z being open Subset of REAL st Z c= dom ((tan - cot) / exp_R) holds
( (tan - cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((tan - cot) / exp_R) implies ( (tan - cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) ) ) )
A1: for x being Real st x in Z holds
exp_R . x <> 0 by SIN_COS:54;
assume  Z c= dom ((tan - cot) / exp_R) ; ::_thesis: ( (tan - cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) ) )
then  Z c= (dom (tan - cot)) /\ ((dom exp_R) \ (exp_R " {0})) by RFUNCT_1:def_1;
then A2: Z c= dom (tan - cot) by XBOOLE_1:18;
then A3: tan - cot is_differentiable_on Z by Th5;
A4: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16;
then A5: (tan - cot) / exp_R is_differentiable_on Z by A3, A1, FDIFF_2:21;
 for x being Real st x in Z holds
(((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x)
proof
let x be Real; ::_thesis: ( x in Z implies (((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) )
A6: exp_R is_differentiable_in x by SIN_COS:65;
A7: exp_R . x <> 0 by SIN_COS:54;
assume A8: x in Z ; ::_thesis: (((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x)
then A9: (tan - cot) . x = (tan . x) - (cot . x) by A2, VALUED_1:13;
 tan - cot is_differentiable_in x by A3, A8, FDIFF_1:9;
then  diff (((tan - cot) / exp_R),x) = (((diff ((tan - cot),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x))) / ((exp_R . x) ^2) by A6, A7, FDIFF_2:14
.= (((((tan - cot) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x))) / ((exp_R . x) ^2) by A3, A8, FDIFF_1:def_7
.= ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x))) / ((exp_R . x) ^2) by A2, A8, Th5
.= ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * (exp_R . x)) - ((exp_R . x) * ((tan . x) - (cot . x)))) / ((exp_R . x) * (exp_R . x)) by A9, SIN_COS:65
.= (((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) * ((exp_R . x) / ((exp_R . x) * (exp_R . x)))
.= (((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) * (((exp_R . x) / (exp_R . x)) / (exp_R . x)) by XCMPLX_1:78
.= (((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) * (1 / (exp_R . x)) by A7, XCMPLX_1:60
.= (((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) / (exp_R . x) ;
hence  (((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) by A5, A8, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( (tan - cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(((tan - cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) ) ) by A3, A4, A1, FDIFF_2:21; ::_thesis: verum
end;

theorem :: FDIFF_10:42
for Z being open Subset of REAL st Z c= dom ((tan + cot) / exp_R) holds
( (tan + cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((tan + cot) / exp_R) implies ( (tan + cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) ) ) )
A1: for x being Real st x in Z holds
exp_R . x <> 0 by SIN_COS:54;
assume  Z c= dom ((tan + cot) / exp_R) ; ::_thesis: ( (tan + cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) ) )
then  Z c= (dom (tan + cot)) /\ ((dom exp_R) \ (exp_R " {0})) by RFUNCT_1:def_1;
then A2: Z c= dom (tan + cot) by XBOOLE_1:18;
then A3: tan + cot is_differentiable_on Z by Th6;
A4: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16;
then A5: (tan + cot) / exp_R is_differentiable_on Z by A3, A1, FDIFF_2:21;
 for x being Real st x in Z holds
(((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x)
proof
let x be Real; ::_thesis: ( x in Z implies (((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) )
A6: exp_R is_differentiable_in x by SIN_COS:65;
A7: exp_R . x <> 0 by SIN_COS:54;
assume A8: x in Z ; ::_thesis: (((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x)
then A9: (tan + cot) . x = (tan . x) + (cot . x) by A2, VALUED_1:def_1;
 tan + cot is_differentiable_in x by A3, A8, FDIFF_1:9;
then  diff (((tan + cot) / exp_R),x) = (((diff ((tan + cot),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x))) / ((exp_R . x) ^2) by A6, A7, FDIFF_2:14
.= (((((tan + cot) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x))) / ((exp_R . x) ^2) by A3, A8, FDIFF_1:def_7
.= ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x))) / ((exp_R . x) ^2) by A2, A8, Th6
.= ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) * (exp_R . x)) - ((exp_R . x) * ((tan . x) + (cot . x)))) / ((exp_R . x) * (exp_R . x)) by A9, SIN_COS:65
.= (((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - ((tan . x) + (cot . x))) * ((exp_R . x) / ((exp_R . x) * (exp_R . x)))
.= (((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - ((tan . x) + (cot . x))) * (((exp_R . x) / (exp_R . x)) / (exp_R . x)) by XCMPLX_1:78
.= (((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - ((tan . x) + (cot . x))) * (1 / (exp_R . x)) by A7, XCMPLX_1:60
.= (((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - ((tan . x) + (cot . x))) / (exp_R . x) ;
hence  (((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) by A5, A8, FDIFF_1:def_7; ::_thesis: verum
end;
hence  ( (tan + cot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(((tan + cot) / exp_R) `| Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) ) ) by A3, A4, A1, FDIFF_2:21; ::_thesis: verum
end;

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

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

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

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