f . (0. V) = 0. K by HAHNBAN1:def 13;
then 0. V in ker f ;
hence not ker f is empty ; :: thesis: verum