A1: |[1,0 ]| `2 = 0 by EUCLID:56;
A2: |[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 A2, A1, JGRAPH_1:47
.= 1 by SQUARE_1:89 ;
hence |[1,0 ]| is Point of (Tunit_circle 2) by Lm13, TOPREAL9:9; :: thesis: verum