set A = { v where v is Element of S : f . v = 0. Z } ;
{ v where v is Element of S : f . v = 0. Z } c= the carrier of S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of S : f . v = 0. Z } or x in the carrier of S )
assume x in { v where v is Element of S : f . v = 0. Z } ; :: thesis: x in the carrier of S
then ex v being Element of S st
( v = x & f . v = 0. Z ) ;
hence x in the carrier of S ; :: thesis: verum

end;

hence { v where v is Element of S : f . v = 0. Z } is Subset of S ; :: thesis: verum