let h, x be Real; :: thesis: ( x + (h / 2) in dom tan & x - (h / 2) in dom tan implies (cD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2))) )
set f = (tan (#) tan) (#) cos;
assume A1: ( x + (h / 2) in dom tan & x - (h / 2) in dom tan ) ; :: thesis: (cD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2)))
( x + (h / 2) in dom ((tan (#) tan) (#) cos) & x - (h / 2) in dom ((tan (#) tan) (#) cos) )

proof

set f1 = tan (#) tan;
set f2 = cos ;
A2: ( x + (h / 2) in dom (tan (#) tan) & x - (h / 2) in dom (tan (#) tan) )

proof

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

end;

( x + (h / 2) in (dom (tan (#) tan)) /\ (dom cos) & x - (h / 2) in (dom (tan (#) tan)) /\ (dom cos) ) by A2, SIN_COS:24, XBOOLE_0:def 4;
hence ( x + (h / 2) in dom ((tan (#) tan) (#) cos) & x - (h / 2) in dom ((tan (#) tan) (#) cos) ) by VALUED_1:def 4; :: thesis: verum

end;

then (cD (((tan (#) tan) (#) cos),h)) . x = (((tan (#) tan) (#) cos) . (x + (h / 2))) - (((tan (#) tan) (#) cos) . (x - (h / 2))) by DIFF_1:39
.= (((tan (#) tan) . (x + (h / 2))) * (cos . (x + (h / 2)))) - (((tan (#) tan) (#) cos) . (x - (h / 2))) by VALUED_1:5
.= (((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((tan (#) tan) (#) cos) . (x - (h / 2))) by VALUED_1:5
.= (((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((tan (#) tan) . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= (((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= ((((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) ")) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def 1
.= ((((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) ")) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - ((((sin . (x - (h / 2))) * ((cos . (x - (h / 2))) ")) * (tan . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def 1
.= (((sin . (x + (h / 2))) * (tan . (x + (h / 2)))) * ((cos . (x + (h / 2))) * (1 / (cos . (x + (h / 2)))))) - (((sin . (x - (h / 2))) * (tan . (x - (h / 2)))) * ((cos . (x - (h / 2))) * (1 / (cos . (x - (h / 2))))))
.= (((sin . (x + (h / 2))) * (tan . (x + (h / 2)))) * 1) - (((sin . (x - (h / 2))) * (tan . (x - (h / 2)))) * ((cos . (x - (h / 2))) * (1 / (cos . (x - (h / 2)))))) by A1, FDIFF_8:1, XCMPLX_1:106
.= (((sin . (x + (h / 2))) * (tan . (x + (h / 2)))) * 1) - (((sin . (x - (h / 2))) * (tan . (x - (h / 2)))) * 1) by A1, FDIFF_8:1, XCMPLX_1:106
.= ((tan (#) sin) . (x + (h / 2))) - ((tan . (x - (h / 2))) * (sin . (x - (h / 2)))) by VALUED_1:5
.= ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2))) by VALUED_1:5 ;
hence (cD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2))) ; :: thesis: verum