let n be set ; :: thesis: for L being non empty ZeroStr
for c being ConstPoly of n,L holds
( term c = EmptyBag n & coefficient c = c . () )

let L be non empty ZeroStr ; :: thesis: for c being ConstPoly of n,L holds
( term c = EmptyBag n & coefficient c = c . () )

let c be ConstPoly of n,L; :: thesis: ( term c = EmptyBag n & coefficient c = c . () )
set eb = EmptyBag n;
A1: now :: thesis: ( ( c . () <> 0. L & term c = EmptyBag n ) or ( c . () = 0. L & term c = EmptyBag n ) )
per cases ( c . () <> 0. L or c . () = 0. L ) ;
case A2: c . () = 0. L ; :: thesis:
Support c = {}
proof
set u = the Element of Support c;
assume A3: Support c <> {} ; :: thesis: contradiction
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 ;
hence contradiction by A2, Def7; :: thesis: verum
end;
hence term c = EmptyBag n by Def5; :: thesis: verum
end;
end;
end;
hence term c = EmptyBag n ; :: thesis: coefficient c = c . ()
thus coefficient c = c . () by A1; :: thesis: verum