set f = sin | [.(- (PI / 2)),(PI / 2).];
A1: (sin | [.(- (PI / 2)),(PI / 2).]) .: [.(- (PI / 2)),(PI / 2).] = [.(- 1),1.] by Th45, RELAT_1:162;
(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 increasing by FCONT_3:17;
hence arcsin | [.(- 1),1.] is increasing by A1, RELAT_1:101; :: thesis: verum