( f . (0. V),(0. V) = 0. K & diagker f = { v where v is Vector of V : f . v,v = 0. K } ) by Th34;
then 0. V in diagker f ;
hence not diagker f is empty ; :: thesis: verum