set f = sin | [.(- (PI / 2)),(PI / 2).];
dom (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- (PI / 2)),(PI / 2).] by RELAT_1:62, SIN_COS:24;
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:23, FCONT_1:47, RELAT_1:73;
hence arcsin | [.(- 1),1.] is continuous by COMPTRIG:30, RELAT_1:115; :: thesis: verum