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