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