let R be domRing; :: thesis: for n being non empty Ordinal holds Zero_ ([#] (Polynom-Ring (n,R))) = {} (Funcs (n,([#] R)))
let n be non empty Ordinal; :: thesis: Zero_ ([#] (Polynom-Ring (n,R))) = {} (Funcs (n,([#] R)))
Zero_ ([#] (Polynom-Ring (n,R))) = Zero_ ({(1. (Polynom-Ring (n,R)))} -Ideal) by RING_2:20
.= Zero_ {(1. (Polynom-Ring (n,R)))} by Th17
.= Zero_ {(1_ (n,R))} by POLYNOM1:31
.= Zero_ (1_ (n,R)) by Th15
.= {} (Funcs (n,([#] R))) by Th14 ;
hence Zero_ ([#] (Polynom-Ring (n,R))) = {} (Funcs (n,([#] R))) ; :: thesis: verum