let L be non empty non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for n being Ordinal
for p being Polynomial of n,L st Support p = {} holds
p = 0_ n,L
let n be Ordinal; :: thesis: for p being Polynomial of n,L st Support p = {} holds
p = 0_ n,L
let p be Polynomial of n,L; :: thesis: ( Support p = {} implies p = 0_ n,L )
assume A1: Support p = {} ; :: thesis: p = 0_ n,L
A2: for u being set st u in Bags n holds
p . u = (0_ n,L) . u

proof

let u be set ; :: thesis: ( u in Bags n implies p . u = (0_ n,L) . u )
assume A3: u in Bags n ; :: thesis: p . u = (0_ n,L) . u
then reconsider b = u as bag of n ;
p . b = 0. L by A1, A3, POLYNOM1:def 9;
hence p . u = (0_ n,L) . u by POLYNOM1:81; :: thesis: verum

end;

A4: Bags n = dom (0_ n,L) by FUNCT_2:def 1;
Bags n = dom p by FUNCT_2:def 1;
hence p = 0_ n,L by A4, A2, FUNCT_1:9; :: thesis: verum