let R be domRing; for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds X c= Zero_ (Ideal_ X)
let n be non empty Ordinal; for X being Subset of (Funcs (n,([#] R))) holds X c= Zero_ (Ideal_ X)
let X be Subset of (Funcs (n,([#] R))); X c= Zero_ (Ideal_ X)
for o being object st o in X holds
o in Zero_ (Ideal_ X)
proof
let o be
object ;
( o in X implies o in Zero_ (Ideal_ X) )
assume A1:
o in X
;
o in Zero_ (Ideal_ X)
then reconsider X =
X as non
empty Subset of
(Funcs (n,([#] R))) by XBOOLE_0:def 1;
consider x being
Function such that A2:
(
o = x &
dom x = n &
rng x c= [#] R )
by A1, FUNCT_2:def 2;
reconsider x =
x as
Function of
n,
R by A2, FUNCT_2:2;
o in Zero_ (Ideal_ X)
proof
assume
not
o in Zero_ (Ideal_ X)
;
contradiction
then
not
o in { z where z is Function of n,R : for f being Polynomial of n,R st f in Ideal_ X holds
eval (f,z) = 0. R }
by Def6;
then consider f1 being
Polynomial of
n,
R such that A4:
(
f1 in Ideal_ X &
eval (
f1,
x)
<> 0. R )
by A2;
consider f2 being
Polynomial of
n,
R such that A5:
(
f1 = f2 &
X c= Zero_ f2 )
by A4;
o in Zero_ f1
by A1, A5;
then consider x1 being
Function of
n,
R such that A6:
(
x1 = o &
eval (
f1,
x1)
= 0. R )
;
thus
contradiction
by A2, A4, A6;
verum
end;
hence
o in Zero_ (Ideal_ X)
;
verum
end;
hence
X c= Zero_ (Ideal_ X)
; verum