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