( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 & <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 ) ;
then |(<e2>,<e3>)| = ((0 * 0) + (1 * 0)) + (0 * 1) by Lm5
.= 0 ;
hence <e2> , <e3> are_orthogonal ; :: thesis: verum