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