( dom sin = REAL & sin | REAL is continuous ) by Th67, FDIFF_1:25, FUNCT_2:def 1;
hence sin is continuous by RELAT_1:69; :: thesis: verum