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

proof

set f1 = cot (#) cot;
set f2 = sin ;
A2: ( x in dom (cot (#) cot) & x + h in dom (cot (#) cot) )

proof

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

end;

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

end;

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