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