let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for n being Ordinal holds Support (0_ (n,L)) = {}
let n be Ordinal; :: thesis: Support (0_ (n,L)) = {}
assume Support (0_ (n,L)) <> {} ; :: thesis: contradiction
then consider o being object such that
A2: o in Support (0_ (n,L)) by XBOOLE_0:def 1;
reconsider b = o as bag of n by A2;
( b in dom (0_ (n,L)) & (0_ (n,L)) . b <> 0. L ) by A2, POLYNOM1:def 3;
hence contradiction by POLYNOM1:22; :: thesis: verum