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

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