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

then
0. V in leftker f
;let w be Vector of W; :: thesis: f . ((0. V),w) = 0. K

thus f . ((0. V),w) = (FunctionalSAF (f,w)) . (0. V) by Th9

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

end;thus f . ((0. V),w) = (FunctionalSAF (f,w)) . (0. V) by Th9

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

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