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

proof

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

end;

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