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

then
0. W in rightker f
;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;thus f . (v,(0. W)) = (FunctionalFAF (f,v)) . (0. W) by Th8

.= 0. K by HAHNBAN1:def 9 ; :: thesis: verum

hence not rightker f is empty ; :: thesis: verum