A1:
|[1,0]| `2 = 0
by EUCLID:52;
A2:
|[1,0]| `1 = 1
by EUCLID:52;
|.(|[(1 + 0),(0 + 0)]| - |[0,0]|).| =
|.((|[1,0]| + |[0,0]|) - |[0,0]|).|
by EUCLID:56
.=
|.(|[1,0]| + (|[0,0]| - |[0,0]|)).|
by RLVECT_1:def 3
.=
|.(|[1,0]| + (0. (TOP-REAL 2))).|
by RLVECT_1:5
.=
|.|[1,0]|.|
by RLVECT_1:4
.=
sqrt ((1 ^2) + (0 ^2))
by A2, A1, JGRAPH_1:30
.=
1
by SQUARE_1:22
;
hence
|[1,0]| is Point of (Tunit_circle 2)
by Lm13, TOPREAL9:9; verum