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

proof

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

end;

ex f being Function of the carrier of I[01],(Tunit_circle 3) st
for x being Element of I[01] holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
hence ex b₁ being Function of I[01],(Tunit_circle 3) st
for x being Point of I[01] holds b₁ . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x)),0]| ; :: thesis: verum