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