let A, B, C be Point of (TOP-REAL 2); :: thesis: for r being positive Real st not angle (A,B,C) is zero holds
sin (r * (angle (C,B,A))) = ((sin ((r * 2) * PI)) * (cos (r * (angle (A,B,C))))) - ((cos ((r * 2) * PI)) * (sin (r * (angle (A,B,C)))))
let r be positive Real; :: thesis: ( not angle (A,B,C) is zero implies sin (r * (angle (C,B,A))) = ((sin ((r * 2) * PI)) * (cos (r * (angle (A,B,C))))) - ((cos ((r * 2) * PI)) * (sin (r * (angle (A,B,C))))) )
assume not angle (A,B,C) is zero ; :: thesis: sin (r * (angle (C,B,A))) = ((sin ((r * 2) * PI)) * (cos (r * (angle (A,B,C))))) - ((cos ((r * 2) * PI)) * (sin (r * (angle (A,B,C)))))
then angle (C,B,A) = (2 * PI) - (angle (A,B,C)) by EUCLID_3:37;
then r * (angle (C,B,A)) = ((r * 2) * PI) - (r * (angle (A,B,C))) ;
hence sin (r * (angle (C,B,A))) = ((sin ((r * 2) * PI)) * (cos (r * (angle (A,B,C))))) - ((cos ((r * 2) * PI)) * (sin (r * (angle (A,B,C))))) by SIN_COS:82; :: thesis: verum