set Z = { x where x is Function of n,R : for p being Polynomial of n,R st p in S holds
eval (p,x) = 0. R } ;
{ x where x is Function of n,R : for p being Polynomial of n,R st p in S holds
eval (p,x) = 0. R } c= Funcs (n,([#] R))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { x where x is Function of n,R : for p being Polynomial of n,R st p in S holds
eval (p,x) = 0. R } or z in Funcs (n,([#] R)) )
assume z in { x where x is Function of n,R : for p being Polynomial of n,R st p in S holds
eval (p,x) = 0. R } ; :: thesis: z in Funcs (n,([#] R))
then consider x being Function of n,R such that
A2: ( z = x & ( for p being Polynomial of n,R st p in S holds
eval (p,x) = 0. R ) ) ;
thus z in Funcs (n,([#] R)) by A2, FUNCT_2:8; :: thesis: verum

end;

hence ( ( S <> {} implies { x where x is Function of n,R : for p being Polynomial of n,R st p in S holds
eval (p,x) = 0. R } is Subset of (Funcs (n,([#] R))) ) & ( not S <> {} implies {} is Subset of (Funcs (n,([#] R))) ) ) by XBOOLE_1:2; :: thesis: verum