A3:
|[(- 1),0]| `2 = 0
by EUCLID:52;
A4:
|[(- 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 A4, A3, JGRAPH_1:30
.=
sqrt ((1 ^2) + (0 ^2))
.=
1
by SQUARE_1:22
;
hence
|[(- 1),0]| is Point of (Tunit_circle 2)
by Lm13, TOPREAL9:9; verum