now

let v be Vector of V; :: thesis: f . v,(0. W) = 0. K
thus f . v,(0. W) = (FunctionalFAF f,v) . (0. W) by Th9
.= 0. K by HAHNBAN1:def 13 ; :: thesis: verum

end;

then 0. W in rightker f ;
hence not rightker f is empty ; :: thesis: verum