let L be 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 object st u in Bags n holds
p . u = (0_ (n,L)) . u

proof

let u be object ; :: 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 4;
hence p . u = (0_ (n,L)) . u by POLYNOM1:22; :: 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:2; :: thesis: verum