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