defpred S1[ Real, set ] means \$2 = |[(cos (((2 * PI) * r) * \$1)),(sin (((2 * PI) * r) * \$1))]|;
A1: for x being Element of I[01] ex y being Element of the carrier of () st S1[x,y]
proof
let x be Element of I[01]; :: thesis: ex y being Element of the carrier of () st S1[x,y]
set y = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]|;
|.(|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| - ).| = |.|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]|.| by
.= sqrt (((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| `1) ^2) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| `2) ^2)) by JGRAPH_1:30
.= sqrt (((cos (((2 * PI) * r) * x)) ^2) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| `2) ^2)) by EUCLID:52
.= sqrt (((cos (((2 * PI) * r) * x)) ^2) + ((sin (((2 * PI) * r) * x)) ^2)) by EUCLID:52
.= 1 by ;
then reconsider y = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| as Element of the carrier of () by ;
take y ; :: thesis: S1[x,y]
thus S1[x,y] ; :: thesis: verum
end;
ex f being Function of the carrier of I[01], the carrier of () st
for x being Element of I[01] holds S1[x,f . x] from hence ex b1 being Function of I[01],() st
for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ; :: thesis: verum