set A = { w where w is Vector of W : for v being Vector of V holds f . v,w = 0. K } ;
{ w where w is Vector of W : for v being Vector of V holds f . v,w = 0. K } c= the carrier of W

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Vector of W : for v being Vector of V holds f . v,w = 0. K } or x in the carrier of W )
assume x in { w where w is Vector of W : for v being Vector of V holds f . v,w = 0. K } ; :: thesis: x in the carrier of W
then consider w being Vector of W such that
A1: ( w = x & ( for v being Vector of V holds f . v,w = 0. K ) ) ;
thus x in the carrier of W by A1; :: thesis: verum

end;

hence { w where w is Vector of W : for v being Vector of V holds f . v,w = 0. K } is Subset of W ; :: thesis: verum