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; :: thesis: verum

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; :: thesis: verum