A1: R^1 | ([#] R^1) = R^1 by TSEP_1:3;
CircleMap | REAL = CircleMap by Lm18, RELAT_1:69;
hence CircleMap is onto by A1, Th38, TOPMETR:17; :: thesis: verum