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;

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

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 ) )end;

hence
term c = EmptyBag n
; :: thesis: coefficient c = c . (EmptyBag n)per cases
( c . (EmptyBag n) <> 0. L or c . (EmptyBag n) = 0. L )
;

end;

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

Support c = {}

end;proof

hence
term c = EmptyBag n
by Def5; :: thesis: verum
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;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

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