theorem :: DIFF_3:77

for x0, x1 being Real st x0 in dom tan & x1 in dom tan holds
[!(tan (#) sin),x0,x1!] = ((((1 / (cos x0)) - (cos x0)) - (1 / (cos x1))) + (cos x1)) / (x0 - x1)