let R be domRing; :: thesis: for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds
( X = {} iff Ideal_ X = [#] (Polynom-Ring (n,R)) )
let n be non empty Ordinal; :: thesis: for X being Subset of (Funcs (n,([#] R))) holds
( X = {} iff Ideal_ X = [#] (Polynom-Ring (n,R)) )
let X be Subset of (Funcs (n,([#] R))); :: thesis: ( X = {} iff Ideal_ X = [#] (Polynom-Ring (n,R)) )
A1: ( X = {} implies Ideal_ X = [#] (Polynom-Ring (n,R)) )

proof

assume A2: X = {} ; :: thesis: Ideal_ X = [#] (Polynom-Ring (n,R))
for o being object st o in [#] (Polynom-Ring (n,R)) holds
o in Ideal_ X

proof

let o be object ; :: thesis: ( o in [#] (Polynom-Ring (n,R)) implies o in Ideal_ X )
assume o in [#] (Polynom-Ring (n,R)) ; :: thesis: o in Ideal_ X
then reconsider f = o as Polynomial of n,R by POLYNOM1:def 11;
{} c= Zero_ f by XBOOLE_1:2;
hence o in Ideal_ X by A2; :: thesis: verum

end;

then [#] (Polynom-Ring (n,R)) c= Ideal_ X ;
hence Ideal_ X = [#] (Polynom-Ring (n,R)) ; :: thesis: verum

end;

( Ideal_ X = [#] (Polynom-Ring (n,R)) implies X = {} (Funcs (n,([#] R))) )

proof

assume A4: Ideal_ X = [#] (Polynom-Ring (n,R)) ; :: thesis: X = {} (Funcs (n,([#] R)))
assume X <> {} (Funcs (n,([#] R))) ; :: thesis: contradiction
then consider o being object such that
A6: o in X by XBOOLE_0:def 1;
reconsider x = o as Element of Funcs (n,([#] R)) by A6;
A7: Ideal_ {x} = [#] (Polynom-Ring (n,R)) by A4, Th29, A6, ZFMISC_1:31;
reconsider y = x as Function of n,R ;
1. (Polynom-Ring (n,R)) in [#] (Polynom-Ring (n,R)) by SUBSET_1:def 1;
then 1_ (n,R) in { f where f is Polynomial of n,R : {x} c= Zero_ f } by A7, POLYNOM1:31;
then consider g being Polynomial of n,R such that
A9: ( g = 1_ (n,R) & {x} c= Zero_ g ) ;
{x} c= {} (Funcs (n,([#] R))) by A9, Th14;
hence contradiction ; :: thesis: verum

end;

hence ( X = {} iff Ideal_ X = [#] (Polynom-Ring (n,R)) ) by A1; :: thesis: verum