A1: cos = R^1 cos ;
R^1 | (R^1 (dom cos)) = R^1 by Th6, SIN_COS:24;
hence cos is Function of R^1,R^1 by A1, COMPTRIG:29, TOPREALA:7; :: thesis: verum