A1: sin = R^1 sin ;
R^1 | (R^1 (dom sin )) = R^1 by Th6, SIN_COS:27;
hence sin is Function of R^1 ,R^1 by A1, COMPTRIG:46, TOPREALA:28; :: thesis: verum