let R be domRing; :: thesis: for n being non empty Ordinal
for X being Algebraic_Set of n,R holds X = Zero_ (Ideal_ X)
let n be non empty Ordinal; :: thesis: for X being Algebraic_Set of n,R holds X = Zero_ (Ideal_ X)
let X be Algebraic_Set of n,R; :: thesis: X = Zero_ (Ideal_ X)
consider I being Ideal of (Polynom-Ring (n,R)) such that
A1: X = Zero_ I by Def7;
thus X = Zero_ (Ideal_ X) by A1, Th34; :: thesis: verum