sin | [.((- (PI / 2)) + H₁(1)),((PI / 2) + H₁(1)).] is one-to-one by Th57;
hence sin | [.((3 / 2) * PI),(2 * PI).] is one-to-one by Lm8, Th2, XXREAL_1:34; :: thesis: verum