now :: thesis: for v being Vector of V holds f . (v,(0. W)) = 0. K

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

end;

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