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

proof

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

end;

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