defpred S₁[ Real, 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:54, RLVECT_1:13
.= sqrt (((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| `1) ^2) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| `2) ^2)) by JGRAPH_1:30
.= sqrt (((cos ((2 * PI) * x)) ^2) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| `2) ^2)) by EUCLID:52
.= sqrt (((cos ((2 * PI) * x)) ^2) + ((sin ((2 * PI) * x)) ^2)) by EUCLID:52
.= 1 by SIN_COS:29, SQUARE_1:18 ;
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 holds f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|
let x be Real; :: thesis: f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|
x is Point of R^1 by TOPMETR:17, XREAL_0:def 1;
hence f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| by A2; :: thesis: verum