f . (0. X) = 0. X9 by Th35;
then 0. X in Ker f ;
hence not Ker f is empty ; :: thesis: verum