A2: ( dom cos = REAL & cos | REAL is continuous ) by Th72, FDIFF_1:33, FUNCT_2:def 1;
thus cos is continuous by A2, RELAT_1:98; :: thesis: verum