A3:
|[(- 1),0 ]| `2 = 0
by EUCLID:56;
A4:
|[(- 1),0 ]| `1 = - 1
by EUCLID:56;
|.(|[((- 1) + 0 ),(0 + 0 )]| - |[0 ,0 ]|).| =
|.((|[(- 1),0 ]| + |[0 ,0 ]|) - |[0 ,0 ]|).|
by EUCLID:60
.=
|.(|[(- 1),0 ]| + (|[0 ,0 ]| - |[0 ,0 ]|)).|
by EUCLID:49
.=
|.(|[(- 1),0 ]| + (0. (TOP-REAL 2))).|
by EUCLID:46
.=
|.|[(- 1),0 ]|.|
by EUCLID:31
.=
sqrt (((- 1) ^2 ) + (0 ^2 ))
by A4, A3, JGRAPH_1:47
.=
sqrt ((1 ^2 ) + (0 ^2 ))
.=
1
by SQUARE_1:89
;
hence
|[(- 1),0 ]| is Point of (Tunit_circle 2)
by Lm13, TOPREAL9:9; verum