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