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

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