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

proof

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

proof

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

end;

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

end;

then (cD (((cot (#) cot) (#) cos),h)) . x = (((cot (#) cot) (#) cos) . (x + (h / 2))) - (((cot (#) cot) (#) cos) . (x - (h / 2))) by DIFF_1:39
.= (((cot (#) cot) . (x + (h / 2))) * (cos . (x + (h / 2)))) - (((cot (#) cot) (#) cos) . (x - (h / 2))) by VALUED_1:5
.= (((cot (#) cot) . (x + (h / 2))) * (cos . (x + (h / 2)))) - (((cot (#) cot) . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= (((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((cot (#) cot) . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= (((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * (cot . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def 1
.= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) * (cos . (x + (h / 2)))) - (((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def 1
.= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) * (cos . (x + (h / 2)))) - ((((cos . (x - (h / 2))) * ((sin . (x - (h / 2))) ")) * (cot . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def 1
.= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) * (cos . (x + (h / 2)))) - ((((cos . (x - (h / 2))) * ((sin . (x - (h / 2))) ")) * ((cos . (x - (h / 2))) * ((sin . (x - (h / 2))) "))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def 1
.= ((((cos . (x + (h / 2))) * (cos . (x + (h / 2)))) * (cos . (x + (h / 2)))) * (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) ")))
.= (((((cos . (x + (h / 2))) |^ 1) * (cos . (x + (h / 2)))) * (cos . (x + (h / 2)))) * (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) ")))
.= ((((cos . (x + (h / 2))) |^ (1 + 1)) * (cos . (x + (h / 2)))) * (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6
.= (((cos . (x + (h / 2))) |^ (2 + 1)) * (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6
.= (((cos . (x + (h / 2))) |^ 3) * ((((sin . (x + (h / 2))) ") |^ 1) * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) ")))
.= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ (1 + 1))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6
.= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((((cos . (x - (h / 2))) |^ 1) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) ")))
.= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - ((((cos . (x - (h / 2))) |^ (1 + 1)) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6
.= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ (2 + 1)) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6
.= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * ((((sin . (x - (h / 2))) ") |^ 1) * ((sin . (x - (h / 2))) ")))
.= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ (1 + 1))) by NEWTON:6
.= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ 2)) ;
hence (cD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ 2)) ; :: thesis: verum