|(<e3>,<e3>)| = ((0 ^2) + (0 ^2)) + (1 ^2) by Lm12
.= 1 ;
hence |.<e3>.| = 1 ; :: thesis: verum