let n be set ; :: thesis:
let L be non empty ZeroStr ; :: thesis:
let c be ConstPoly of n,L; :: thesis:
set eb = EmptyBag n;

A1: now :: thesis:

case c . (EmptyBag n) <> 0. L ; :: thesis:

hence term c = EmptyBag n by Def5; :: thesis:

end;

case A2: c . (EmptyBag n) = 0. L ; :: thesis:

set u = the Element of Support c;
assume A3: Support c <> {} ; :: thesis:
then the Element of Support c in Support c ;
then reconsider u = the Element of Support c as Element of Bags n ;
c . u <> 0. L by A3, POLYNOM1:def 4;
hence contradiction by A2, Def7; :: thesis:

end;

hence term c = EmptyBag n by Def5; :: thesis:

end;

end;

end;

hence term c = EmptyBag n ; :: thesis:
thus coefficient c = c . (EmptyBag n) by A1; :: thesis: