A1: R^1 | ([#] R^1 ) = R^1 by TSEP_1:3;
CircleMap | REAL = CircleMap by Lm19, RELAT_1:98;
hence CircleMap is onto by A1, Th39, TOPMETR:24; :: thesis: verum