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