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