defpred S₁[ real number , set ] means $2 = |[(cos ((2 * PI ) * $1)),(sin ((2 * PI ) * $1))]|;
A1: for x being Element of R^1 ex y being Element of the carrier of (Tunit_circle 2) st S₁[x,y]

proof

let x be Element of R^1 ; :: thesis: ex y being Element of the carrier of (Tunit_circle 2) st S₁[x,y]
set y = |[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]|;
|.(|[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]| - |[0 ,0 ]|).| = |.|[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]|.| by EUCLID:58, RLVECT_1:26
.= sqrt (((|[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]| `1 ) ^2 ) + ((|[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]| `2 ) ^2 )) by JGRAPH_1:47
.= sqrt (((cos ((2 * PI ) * x)) ^2 ) + ((|[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]| `2 ) ^2 )) by EUCLID:56
.= sqrt (((cos ((2 * PI ) * x)) ^2 ) + ((sin ((2 * PI ) * x)) ^2 )) by EUCLID:56
.= 1 by SIN_COS:32, SQUARE_1:83 ;
then |[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]| is Element of the carrier of (Tunit_circle 2) by Lm13, TOPREAL9:9;
hence ex y being Element of the carrier of (Tunit_circle 2) st S₁[x,y] ; :: thesis: verum

end;

consider f being Function of the carrier of R^1 ,the carrier of (Tunit_circle 2) such that
A2: for x being Element of R^1 holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for x being real number holds f . x = |[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]|
let x be real number ; :: thesis: f . x = |[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]|
x is Point of R^1 by TOPMETR:24, XREAL_0:def 1;
hence f . x = |[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]| by A2; :: thesis: verum