set f = sin | [.(- (PI / 2)),(PI / 2).];
A1: dom (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- (PI / 2)),(PI / 2).] by Lm1, RELAT_1:91;
A2: (sin | [.(- (PI / 2)),(PI / 2).]) | [.(- (PI / 2)),(PI / 2).] = sin | [.(- (PI / 2)),(PI / 2).] by RELAT_1:102;
(sin | [.(- (PI / 2)),(PI / 2).]) | [.(- (PI / 2)),(PI / 2).] is increasing by COMPTRIG:39;
then (((sin | [.(- (PI / 2)),(PI / 2).]) | [.(- (PI / 2)),(PI / 2).]) " ) | ((sin | [.(- (PI / 2)),(PI / 2).]) .: [.(- (PI / 2)),(PI / 2).]) is continuous by A1, FCONT_1:54;
hence arcsin | [.(- 1),1.] is continuous by A2, COMPTRIG:48, RELAT_1:148; :: thesis: verum