set F = F_Complex ;
f . ((0. V),(0. V)) = 0. F_Complex by Th42;
then 0. V in diagker f ;
hence not diagker f is empty ; :: thesis: verum