let R be domRing; :: thesis: for n being non empty Ordinal
for x being Element of Funcs (n,([#] R)) holds {x} is Algebraic_Set of n,R
let n be non empty Ordinal; :: thesis: for x being Element of Funcs (n,([#] R)) holds {x} is Algebraic_Set of n,R
let x be Element of Funcs (n,([#] R)); :: thesis: {x} is Algebraic_Set of n,R
x in Funcs (n,([#] R)) by SUBSET_1:def 1;
then consider x1 being Function such that
A1: ( x1 = x & dom x1 = n & rng x1 c= [#] R ) by FUNCT_2:def 2;
reconsider x1 = x1 as Function of n,R by A1;
A2: {x1} = Zero_ (polyset x1) by Th25
.= Zero_ ((polyset x1) -Ideal) by Th17 ;
reconsider Q = {x} as non empty Subset of (Funcs (n,([#] R))) ;
Q is algebraic_set_from_ideal by A2, A1;
hence {x} is Algebraic_Set of n,R ; :: thesis: verum