set p = c1 *' c2;

now

let b be bag of ; :: thesis: ( b <> EmptyBag n implies (c1 *' c2) . b = 0. L )
assume A1: b <> EmptyBag n ; :: thesis: (c1 *' c2) . b = 0. L
consider s being FinSequence of L such that
A2: ( (c1 *' c2) . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of st
( (decomp b) /. k = <*b1,b2*> & s /. k = (c1 . b1) * (c2 . b2) ) ) ) by POLYNOM1:def 26;
A3: dom s = Seg (len (decomp b)) by A2, FINSEQ_1:def 3
.= dom (decomp b) by FINSEQ_1:def 3 ;

A4: now

let k be Element of NAT ; :: thesis: ( k in dom s implies s /. k = 0. L )
assume A5: k in dom s ; :: thesis: s /. k = 0. L
then consider b1, b2 being bag of such that
A6: ( (decomp b) /. k = <*b1,b2*> & s /. k = (c1 . b1) * (c2 . b2) ) by A2;
consider b1', b2' being bag of such that
A7: ( (decomp b) /. k = <*b1',b2'*> & b = b1' + b2' ) by A3, A5, POLYNOM1:72;
A8: b1 = <*b1',b2'*> . 1 by A6, A7, FINSEQ_1:61
.= b1' by FINSEQ_1:61 ;
b2 = <*b1',b2'*> . 2 by A6, A7, FINSEQ_1:61
.= b2' by FINSEQ_1:61 ;
then A9: ( b1 <> EmptyBag n or b2 <> EmptyBag n ) by A1, A7, A8, POLYNOM1:57;

now

per cases ( c1 . b1 = 0. L or c2 . b2 = 0. L ) by A9, POLYNOM7:def 8;

case c1 . b1 = 0. L ; :: thesis: s /. k = 0. L

hence s /. k = 0. L by A6, BINOM:1; :: thesis: verum

end;

case c2 . b2 = 0. L ; :: thesis: s /. k = 0. L

hence s /. k = 0. L by A6, BINOM:2; :: thesis: verum

end;

end;

end;

hence s /. k = 0. L ; :: thesis: verum

end;

now

per cases ( dom s = {} or dom s <> {} ) ;

case dom s = {} ; :: thesis: (c1 *' c2) . b = 0. L

then s = <*> the carrier of L by RELAT_1:64;
hence (c1 *' c2) . b = 0. L by A2; :: thesis: verum

end;

case A10: dom s <> {} ; :: thesis: (c1 *' c2) . b = 0. L

consider k being Element of dom s;
A11: k in dom s by A10;
for k' being Element of NAT st k' in dom s & k' <> k holds
s /. k' = 0. L by A4;
then Sum s = s /. k by A11, POLYNOM2:5;
hence (c1 *' c2) . b = 0. L by A2, A4, A11; :: thesis: verum

end;

end;

end;

hence (c1 *' c2) . b = 0. L ; :: thesis: verum

end;

hence c1 *' c2 is Constant by POLYNOM7:def 8; :: thesis: verum