set M = { x where x is Function of n,R : eval (f,x) = 0. R } ;
{ x where x is Function of n,R : eval (f,x) = 0. R } c= Funcs (n,([#] R))

proof

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

end;

hence { x where x is Function of n,R : eval (f,x) = 0. R } is Subset of (Funcs (n,([#] R))) ; :: thesis: verum