f . ((0. V),(0. V)) = 0. K by Th34;
then 0. V in diagker f ;
hence not diagker f is empty ; :: thesis: verum