dom (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- (PI / 2)),(PI / 2).] by RELAT_1:62, SIN_COS:24;
hence rng arcsin = [.(- (PI / 2)),(PI / 2).] by FUNCT_1:33; :: thesis: verum