set B = |[((sqrt 3) / 2),(1 / 2)]|;
( |[((sqrt 3) / 2),(1 / 2)]| `1 = (sqrt 3) / 2 & |[((sqrt 3) / 2),(1 / 2)]| `2 = 1 / 2 ) by EUCLID:52;
then A1: |.|[((sqrt 3) / 2),(1 / 2)]|.| = sqrt ((((sqrt 3) / 2) ^2) + ((1 / 2) ^2)) by JGRAPH_1:30;
A2: ((sqrt 3) / 2) ^2 = ((sqrt 3) / 2) * ((sqrt 3) / 2) by SQUARE_1:def 1;
A3: (1 / 2) ^2 = (1 / 2) * (1 / 2) by SQUARE_1:def 1;
(sqrt 3) ^2 = 3 by SQUARE_1:def 2;
then (((sqrt 3) * (sqrt 3)) / 2) / 2 = (3 / 2) / 2 by SQUARE_1:def 1;
hence |.|[((sqrt 3) / 2),(1 / 2)]|.| = 1 by A1, A2, A3, SQUARE_1:18; :: thesis: verum