theorem :: SIN_COS6:65
arcsin * (sin | [.(- (PI / 2)),(PI / 2).]) = id [.(- 1),1.] by COMPTRIG:30, FUNCT_1:39;