let a be Real; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (((- (1 / a)) (#) (cosec * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((- (1 / a)) (#) (cosec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) )
let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st Z c= dom (((- (1 / a)) (#) (cosec * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((- (1 / a)) (#) (cosec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) )
let f be PartFunc of REAL,REAL; :: thesis: ( Z c= dom (((- (1 / a)) (#) (cosec * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) implies ( ((- (1 / a)) (#) (cosec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) ) )
assume that
A1: Z c= dom (((- (1 / a)) (#) (cosec * f)) - (id Z)) and
A2: for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ; :: thesis: ( ((- (1 / a)) (#) (cosec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) )
A3: Z c= (dom ((- (1 / a)) (#) (cosec * f))) /\ (dom (id Z)) by A1, VALUED_1:12;
then A4: Z c= dom ((- (1 / a)) (#) (cosec * f)) by XBOOLE_1:18;
then A5: Z c= dom (cosec * f) by VALUED_1:def 5;
A6: for x being Real st x in Z holds
f . x = (a * x) + 0 by A2;
then A7: cosec * f is_differentiable_on Z by A5, Th7;
then A8: (- (1 / a)) (#) (cosec * f) is_differentiable_on Z by A4, FDIFF_1:20;
set g = (- (1 / a)) (#) (cosec * f);
A9: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:18;
A10: Z c= dom (id Z) by A3, XBOOLE_1:18;
then A11: id Z is_differentiable_on Z by A9, FDIFF_1:23;
A12: for x being Real st x in Z holds
sin . (f . x) <> 0

proof

let x be Real; :: thesis: ( x in Z implies sin . (f . x) <> 0 )
assume x in Z ; :: thesis: sin . (f . x) <> 0
then f . x in dom cosec by A5, FUNCT_1:11;
hence sin . (f . x) <> 0 by RFUNCT_1:3; :: thesis: verum

end;

for x being Real st x in Z holds
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2)

proof

let x be Real; :: thesis: ( x in Z implies ((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) )
assume A13: x in Z ; :: thesis: ((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2)
then A14: f . x = (a * x) + 0 by A2;
sin . (f . x) <> 0 by A12, A13;
then A15: (sin . (a * x)) ^2 > 0 by A14, SQUARE_1:12;
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = (diff (((- (1 / a)) (#) (cosec * f)),x)) - (diff ((id Z),x)) by A1, A8, A11, A13, FDIFF_1:19
.= ((((- (1 / a)) (#) (cosec * f)) `| Z) . x) - (diff ((id Z),x)) by A8, A13, FDIFF_1:def 7
.= ((- (1 / a)) * (diff ((cosec * f),x))) - (diff ((id Z),x)) by A4, A7, A13, FDIFF_1:20
.= ((- (1 / a)) * (((cosec * f) `| Z) . x)) - (diff ((id Z),x)) by A7, A13, FDIFF_1:def 7
.= ((- (1 / a)) * (((cosec * f) `| Z) . x)) - (((id Z) `| Z) . x) by A11, A13, FDIFF_1:def 7
.= ((- (1 / a)) * (- ((a * (cos . (a * x))) / ((sin . (a * x)) ^2)))) - (((id Z) `| Z) . x) by A5, A6, A13, A14, Th7
.= (((- 1) / a) * ((a * (- (cos . (a * x)))) / ((sin . (a * x)) ^2))) - 1 by A10, A9, A13, FDIFF_1:23
.= (((- 1) * (a * (- (cos . (a * x))))) / (a * ((sin . (a * x)) ^2))) - 1 by XCMPLX_1:76
.= (((cos . (a * x)) * a) / (((sin . (a * x)) ^2) * a)) - 1
.= ((cos . (a * x)) / ((sin . (a * x)) ^2)) - 1 by A2, A13, XCMPLX_1:91
.= ((cos . (a * x)) / ((sin . (a * x)) ^2)) - (((sin . (a * x)) ^2) / ((sin . (a * x)) ^2)) by A15, XCMPLX_1:60
.= ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ;
hence ((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ; :: thesis: verum

end;

hence ( ((- (1 / a)) (#) (cosec * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cosec * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) ) by A1, A8, A11, FDIFF_1:19; :: thesis: verum