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)) (#) (cot * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((- (1 / a)) (#) (cot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (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)) (#) (cot * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((- (1 / a)) (#) (cot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2 ) / ((sin . (a * x)) ^2 ) ) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( Z c= dom (((- (1 / a)) (#) (cot * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) implies ( ((- (1 / a)) (#) (cot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2 ) / ((sin . (a * x)) ^2 ) ) ) )
assume that
A1: Z c= dom (((- (1 / a)) (#) (cot * f)) - (id Z)) and
A2: for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ; :: thesis: ( ((- (1 / a)) (#) (cot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2 ) / ((sin . (a * x)) ^2 ) ) )
Z c= (dom ((- (1 / a)) (#) (cot * f))) /\ (dom (id Z)) by A1, VALUED_1:12;
then A3: ( Z c= dom ((- (1 / a)) (#) (cot * f)) & Z c= dom (id Z) ) by XBOOLE_1:18;
then A4: Z c= dom (cot * f) by VALUED_1:def 5;
A5: for x being Real st x in Z holds
f . x = (a * x) + 0 by A2;
then A6: ( cot * f is_differentiable_on Z & ( for x being Real st x in Z holds
((cot * f) `| Z) . x = - (a / ((sin . ((a * x) + 0 )) ^2 )) ) ) by A4, Th7;
then A7: ( (- (1 / a)) (#) (cot * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / a)) (#) (cot * f)) `| Z) . x = (- (1 / a)) * (diff (cot * f),x) ) ) by A3, FDIFF_1:28;
A8: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:35;
then A9: ( id Z is_differentiable_on Z & ( for x being Real st x in Z holds
((id Z) `| Z) . x = 1 ) ) by A3, FDIFF_1:31;
A10: 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 (cos / sin ) by A4, FUNCT_1:21;
hence sin . (f . x) <> 0 by Th2; :: thesis: verum

end;

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

proof

let x be Real; :: thesis: ( x in Z implies ((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2 ) / ((sin . (a * x)) ^2 ) )
assume A11: x in Z ; :: thesis: ((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2 ) / ((sin . (a * x)) ^2 )
then A12: ( f . x = (a * x) + 0 & sin . (f . x) <> 0 & a <> 0 ) by A2, A10;
then A13: (sin . (a * x)) ^2 > 0 by SQUARE_1:74;
((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = (diff ((- (1 / a)) (#) (cot * f)),x) - (diff (id Z),x) by A1, A7, A9, A11, FDIFF_1:27
.= ((((- (1 / a)) (#) (cot * f)) `| Z) . x) - (diff (id Z),x) by A7, A11, FDIFF_1:def 8
.= ((- (1 / a)) * (diff (cot * f),x)) - (diff (id Z),x) by A3, A6, A11, FDIFF_1:28
.= ((- (1 / a)) * (((cot * f) `| Z) . x)) - (diff (id Z),x) by A6, A11, FDIFF_1:def 8
.= ((- (1 / a)) * (((cot * f) `| Z) . x)) - (((id Z) `| Z) . x) by A9, A11, FDIFF_1:def 8
.= ((- (1 / a)) * (- (a / ((sin . (a * x)) ^2 )))) - (((id Z) `| Z) . x) by A4, A5, A11, A12, Th7
.= ((1 / ((sin . (a * x)) ^2 )) * (a / a)) - 1 by A3, A8, A11, FDIFF_1:31
.= ((1 / ((sin . (a * x)) ^2 )) * 1) - 1 by A12, XCMPLX_1:60
.= (1 / ((sin . (a * x)) ^2 )) - (((sin . (a * x)) ^2 ) / ((sin . (a * x)) ^2 )) by A13, XCMPLX_1:60
.= (1 - ((sin . (a * x)) ^2 )) / ((sin . (a * x)) ^2 )
.= ((((cos . (a * x)) ^2 ) + ((sin . (a * x)) ^2 )) - ((sin . (a * x)) ^2 )) / ((sin . (a * x)) ^2 ) by SIN_COS:31
.= ((cos . (a * x)) ^2 ) / ((sin . (a * x)) ^2 ) ;
hence ((((- (1 / a)) (#) (cot * f)) - (id Z)) `| Z) . x = ((cos . (a * x)) ^2 ) / ((sin . (a * x)) ^2 ) ; :: thesis: verum

end;

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