sin | [.(- (PI / 2)),0 .] is one-to-one ;
hence sin | ].(- (PI / 2)),0 .[ is one-to-one by Th2, XXREAL_1:25; :: thesis: verum