let h, x be Real; :: thesis: ( x + (h / 2) in dom sec & x - (h / 2) in dom sec implies (cD ((sec (#) sec),h)) . x = ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2) )
set f = sec (#) sec;
assume A1: ( x + (h / 2) in dom sec & x - (h / 2) in dom sec ) ; :: thesis: (cD ((sec (#) sec),h)) . x = ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2)
A2: ( cos . (x + (h / 2)) <> 0 & cos . (x - (h / 2)) <> 0 ) by A1, RFUNCT_1:3;
( x + (h / 2) in dom (sec (#) sec) & x - (h / 2) in dom (sec (#) sec) )

proof

( x + (h / 2) in (dom sec) /\ (dom sec) & x - (h / 2) in (dom sec) /\ (dom sec) ) by A1;
hence ( x + (h / 2) in dom (sec (#) sec) & x - (h / 2) in dom (sec (#) sec) ) by VALUED_1:def 4; :: thesis: verum

end;

then (cD ((sec (#) sec),h)) . x = ((sec (#) sec) . (x + (h / 2))) - ((sec (#) sec) . (x - (h / 2))) by DIFF_1:39
.= ((sec . (x + (h / 2))) * (sec . (x + (h / 2)))) - ((sec (#) sec) . (x - (h / 2))) by VALUED_1:5
.= ((sec . (x + (h / 2))) * (sec . (x + (h / 2)))) - ((sec . (x - (h / 2))) * (sec . (x - (h / 2)))) by VALUED_1:5
.= (((cos . (x + (h / 2))) ") * (sec . (x + (h / 2)))) - ((sec . (x - (h / 2))) * (sec . (x - (h / 2)))) by A1, RFUNCT_1:def 2
.= (((cos . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - ((sec . (x - (h / 2))) * (sec . (x - (h / 2)))) by A1, RFUNCT_1:def 2
.= (((cos . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - (((cos . (x - (h / 2))) ") * (sec . (x - (h / 2)))) by A1, RFUNCT_1:def 2
.= (((cos . (x + (h / 2))) ") ^2) - (((cos . (x - (h / 2))) ") ^2) by A1, RFUNCT_1:def 2
.= ((1 / (cos . (x + (h / 2)))) - (1 / (cos . (x - (h / 2))))) * ((1 / (cos . (x + (h / 2)))) + (1 / (cos . (x - (h / 2)))))
.= (((1 * (cos . (x - (h / 2)))) - (1 * (cos . (x + (h / 2))))) / ((cos . (x + (h / 2))) * (cos . (x - (h / 2))))) * ((1 / (cos . (x + (h / 2)))) + (1 / (cos . (x - (h / 2))))) by A2, XCMPLX_1:130
.= (((cos . (x - (h / 2))) - (cos . (x + (h / 2)))) / ((cos . (x + (h / 2))) * (cos . (x - (h / 2))))) * (((cos . (x - (h / 2))) + (cos . (x + (h / 2)))) / ((cos . (x + (h / 2))) * (cos . (x - (h / 2))))) by A2, XCMPLX_1:116
.= (((cos . (x - (h / 2))) - (cos . (x + (h / 2)))) * ((cos . (x - (h / 2))) + (cos . (x + (h / 2))))) / (((cos . (x + (h / 2))) * (cos . (x - (h / 2)))) * ((cos . (x + (h / 2))) * (cos . (x - (h / 2))))) by XCMPLX_1:76
.= (((cos (x - (h / 2))) * (cos (x - (h / 2)))) - ((cos (x + (h / 2))) * (cos (x + (h / 2))))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2)
.= ((sin ((x + (h / 2)) + (x - (h / 2)))) * (sin ((x + (h / 2)) - (x - (h / 2))))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2) by SIN_COS4:38
.= ((sin (2 * x)) * (sin h)) / (((1 / 2) * ((cos ((x + (h / 2)) + (x - (h / 2)))) + (cos ((x + (h / 2)) - (x - (h / 2)))))) ^2) by SIN_COS4:32
.= (1 * ((sin (2 * x)) * (sin h))) / ((1 / 4) * (((cos (2 * x)) + (cos h)) ^2))
.= (1 / (1 / 4)) * (((sin (2 * x)) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2)) by XCMPLX_1:76
.= ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2) ;
hence (cD ((sec (#) sec),h)) . x = ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2) ; :: thesis: verum