let x0, x1 be Real; :: thesis:
[!(cos (#) cos ),x0,x1!] = (((cos . x0) * (cos . x0)) - ((cos (#) cos ) . x1)) / (x0 - x1) by VALUED_1:5
.= (((cos x0) * (cos x0)) - ((cos x1) * (cos x1))) / (x0 - x1) by VALUED_1:5
.= (((1 / 2) * ((cos (x0 + x0)) + (cos (x0 - x0)))) - ((cos x1) * (cos x1))) / (x0 - x1) by SIN_COS4:36
.= (((1 / 2) * ((cos (x0 + x0)) + (cos (x0 - x0)))) - ((1 / 2) * ((cos (x1 + x1)) + (cos (x1 - x1))))) / (x0 - x1) by SIN_COS4:36
.= (((1 / 2) * (cos (2 * x0))) - ((1 / 2) * (cos (2 * x1)))) / (x0 - x1) ;
hence [!(cos (#) cos ),x0,x1!] = ((1 / 2) * ((cos (2 * x0)) - (cos (2 * x1)))) / (x0 - x1) ; :: thesis: