let R be domRing; :: thesis: for n being non empty Ordinal holds Zero_ (1_ (n,R)) = {} (Funcs (n,([#] R)))
let n be non empty Ordinal; :: thesis: Zero_ (1_ (n,R)) = {} (Funcs (n,([#] R)))
assume Zero_ (1_ (n,R)) <> {} (Funcs (n,([#] R))) ; :: thesis: contradiction
then consider o being object such that
A2: o in Zero_ (1_ (n,R)) by XBOOLE_0:def 1;
consider x being Function of n,R such that
A3: ( o = x & eval ((1_ (n,R)),x) = 0. R ) by A2;
thus contradiction by A3, POLYNOM2:21; :: thesis: verum