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

proof

let x be Element of R^1; :: thesis: ex y being Element of (Tunit_circle 3) st S₁[x,y]
set y = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|;
|.(|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| - |[0,0,0]|).| = |.|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|.| by EUCLID_5:4, RLVECT_1:13
.= sqrt ((((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `1) ^2) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `2) ^2)) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `3) ^2)) by Th25
.= sqrt ((((cos ((2 * PI) * x)) ^2) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `2) ^2)) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `3) ^2)) by EUCLID_5:2
.= sqrt ((((cos ((2 * PI) * x)) ^2) + ((sin ((2 * PI) * x)) ^2)) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| `3) ^2)) by EUCLID_5:2
.= sqrt ((((cos ((2 * PI) * x)) ^2) + ((sin ((2 * PI) * x)) ^2)) + (Q ^2)) by EUCLID_5:2
.= 1 by SIN_COS:29, SQUARE_1:18 ;
then |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| is Element of (Tunit_circle 3) by Lm7, TOPREAL9:9;
hence ex y being Element of (Tunit_circle 3) st S₁[x,y] ; :: thesis: verum

end;

consider f being Function of the carrier of R^1,(Tunit_circle 3) 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)),0]|
let x be Real; :: thesis: f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]|
x is Point of R^1 by TOPMETR:17, XREAL_0:def 1;
hence f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| by A2; :: thesis: verum