set M = [#] (Funcs (n,([#] R)));
Zero_ {(0. (Polynom-Ring (n,R)))} = Zero_ {(0_ (n,R))} by POLYNOM1:def 11
.= Zero_ (0_ (n,R)) by Th15
.= [#] (Funcs (n,([#] R))) by Th13 ;
then [#] (Funcs (n,([#] R))) is algebraic_set_from_ideal ;
hence ex b₁ being non empty Subset of (Funcs (n,([#] R))) st b₁ is algebraic_set_from_ideal ; :: thesis: verum