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

{ 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

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
let x be object ; :: 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 ex v being Vector of V st

( v = x & ( for w being Vector of W holds f . (v,w) = 0. K ) ) ;

hence x in the carrier of V ; :: thesis: verum

end;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 ex v being Vector of V st

( v = x & ( for w being Vector of W holds f . (v,w) = 0. K ) ) ;

hence x in the carrier of V ; :: thesis: verum