let a, b be real number ; :: thesis: |.|[a,b]|.| ^2 = (a ^2 ) + (b ^2 )
( |[a,b]| `1 = a & |[a,b]| `2 = b ) by EUCLID:56;
hence |.|[a,b]|.| ^2 = (a ^2 ) + (b ^2 ) by JGRAPH_1:46; :: thesis: verum