CircleMap | [.r,(r + 1).[ is one-to-one ;
hence CircleMap | ].r,(r + 1).[ is one-to-one by SIN_COS6:2, XXREAL_1:45; :: thesis: verum