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) (#) (tan * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((1 / a) (#) (tan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2 ) / ((cos . (a * x)) ^2 ) ) )
let Z be open Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st Z c= dom (((1 / a) (#) (tan * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) holds
( ((1 / a) (#) (tan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2 ) / ((cos . (a * x)) ^2 ) ) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( Z c= dom (((1 / a) (#) (tan * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ) implies ( ((1 / a) (#) (tan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2 ) / ((cos . (a * x)) ^2 ) ) ) )
assume that
A1: Z c= dom (((1 / a) (#) (tan * f)) - (id Z)) and
A2: for x being Real st x in Z holds
( f . x = a * x & a <> 0 ) ; :: thesis: ( ((1 / a) (#) (tan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / a) (#) (tan * f)) - (id Z)) `| Z) . x = ((sin . (a * x)) ^2 ) / ((cos . (a * x)) ^2 ) ) )
Z c= (dom ((1 / a) (#) (tan * f))) /\ (dom (id Z)) by A1, VALUED_1:12;
then A3: ( Z c= dom ((1 / a) (#) (tan * f)) & Z c= dom (id Z) ) by XBOOLE_1:18;
then A4: Z c= dom (tan * 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: ( tan * f is_differentiable_on Z & ( for x being Real st x in Z holds
((tan * f) `| Z) . x = a / ((cos . ((a * x) + 0 )) ^2 ) ) ) by A4, Th6;
then A7: ( (1 / a) (#) (tan * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / a) (#) (tan * f)) `| Z) . x = (1 / a) * (diff (tan * 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
cos . (f . x) <> 0

proof

let x be Real; :: thesis: ( x in Z implies cos . (f . x) <> 0 )
assume x in Z ; :: thesis: cos . (f . x) <> 0
then f . x in dom (sin / cos ) by A4, FUNCT_1:21;
hence cos . (f . x) <> 0 by Th1; :: thesis: verum

end;

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

proof

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

end;

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