let A be Subset of R^1; :: thesis: CircleMap | A is Function of (R^1 | A),(Tunit_circle 2)
A1: rng (CircleMap | A) c= the carrier of (Tunit_circle 2) ;
dom (CircleMap | A) = A by Lm18, RELAT_1:62, TOPMETR:17
.= the carrier of (R^1 | A) by PRE_TOPC:8 ;
hence CircleMap | A is Function of (R^1 | A),(Tunit_circle 2) by A1, FUNCT_2:2; :: thesis: verum