|(<e2> ,<e2> )| = ((0 ^2 ) + (1 ^2 )) + (0 ^2 ) by LmTh8
.= 1 ;
hence |.<e2> .| = 1 by SQUARE_1:83; :: thesis: verum