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