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