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