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 . (EmptyBag n) )
let L be non empty ZeroStr ; :: thesis: for c being ConstPoly of n,L holds
( term c = EmptyBag n & coefficient c = c . (EmptyBag n) )
let c be ConstPoly of n,L; :: thesis: ( term c = EmptyBag n & coefficient c = c . (EmptyBag n) )
set eb = EmptyBag n;
A1: now :: thesis: ( ( c . (EmptyBag n) <> 0. L & term c = EmptyBag n ) or ( c . (EmptyBag n) = 0. L & term c = EmptyBag n ) )
per cases ( c . (EmptyBag n) <> 0. L or c . (EmptyBag n) = 0. L ) ;
case A2: c . (EmptyBag n) = 0. L ; :: thesis: term c = EmptyBag n
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 A3, POLYNOM1:def 4;
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 . (EmptyBag n)
thus coefficient c = c . (EmptyBag n) by A1; :: thesis: verum