( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 & <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 ) by FINSEQ_1:62;
then |(<e1> ,<e3> )| = ((1 * 0 ) + (0 * 0 )) + (0 * 1) by Lm8
.= 0 ;
hence <e1> , <e3> are_orthogonal by RVSUM_1:def 18; :: thesis: verum