set p = |[1,0,0]|;
|.(|[1,0,0]| - (0. (TOP-REAL 3))).| =
|.|[1,0,0]|.|
by RLVECT_1:13
.=
sqrt ((((|[1,0,0]| `1) ^2) + ((|[1,0,0]| `2) ^2)) + ((|[1,0,0]| `3) ^2))
by Th25
.=
sqrt (((1 ^2) + ((|[1,0,0]| `2) ^2)) + ((|[1,0,0]| `3) ^2))
by EUCLID_5:2
.=
sqrt (((1 ^2) + (Q ^2)) + ((|[1,0,0]| `3) ^2))
by EUCLID_5:2
.=
1
by EUCLID_5:2, SQUARE_1:18
;
then
|[1,0,0]| in Sphere ((0. (TOP-REAL 3)),1)
by TOPREAL9:9;
hence
|[1,0,0]| is Point of (Tunit_circle 3)
by TOPREALB:9; verum