A1: sin = R^1 sin ;
R^1 | (R^1 (dom sin)) = R^1 by SIN_COS:24, TOPREALB:6;
hence sin is Function of R^1,R^1 by A1; :: thesis: verum