now

let w be Vector of W; :: thesis: f . (0. V),w = 0. K
thus f . (0. V),w = (FunctionalSAF f,w) . (0. V) by Th10
.= 0. K by HAHNBAN1:def 13 ; :: thesis: verum

end;

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