let a, b be Real; :: thesis: |.|[a,b]|.| ^2 = (a ^2) + (b ^2)
A1: |[a,b]| `2 = b by EUCLID:52;
|[a,b]| `1 = a by EUCLID:52;
hence |.|[a,b]|.| ^2 = (a ^2) + (b ^2) by A1, JGRAPH_1:29; :: thesis: verum