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 ;
hence |[1,0]| is Point of (Tunit_circle 2) by Lm13, TOPREAL9:9; :: thesis: verum