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