let R be domRing; :: thesis: for n being non empty Ordinal holds {(0. (Polynom-Ring (n,R)))} c= Ideal_ ([#] (Funcs (n,([#] R))))
let n be non empty Ordinal; :: thesis: {(0. (Polynom-Ring (n,R)))} c= Ideal_ ([#] (Funcs (n,([#] R))))
for o being object st o in {(0. (Polynom-Ring (n,R)))} holds
o in Ideal_ ([#] (Funcs (n,([#] R))))

proof

let o be object ; :: thesis: ( o in {(0. (Polynom-Ring (n,R)))} implies o in Ideal_ ([#] (Funcs (n,([#] R)))) )
assume o in {(0. (Polynom-Ring (n,R)))} ; :: thesis: o in Ideal_ ([#] (Funcs (n,([#] R))))
then A2: o = 0. (Polynom-Ring (n,R)) by TARSKI:def 1
.= 0_ (n,R) by POLYNOM1:def 11 ;
Zero_ (0_ (n,R)) = Funcs (n,([#] R)) by Th13;
hence o in Ideal_ ([#] (Funcs (n,([#] R)))) by A2; :: thesis: verum

end;

hence {(0. (Polynom-Ring (n,R)))} c= Ideal_ ([#] (Funcs (n,([#] R)))) ; :: thesis: verum