cos | [.0 ,PI .] is one-to-one ;
hence cos | ].0 ,PI .[ is one-to-one by Th2, XXREAL_1:25; :: thesis: verum