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

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;

then 0. V in leftker f ;
hence not leftker f is empty ; :: thesis: verum