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