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

{ 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

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

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

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

end;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 ex w being Vector of W st

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

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