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