set p = c1 *' c2;

now :: thesis: for b being bag of n st b <> EmptyBag n holds
(c1 *' c2) . b = 0. L

let b be bag of n; :: 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 and
A3: len s = len (decomp b) and
A4: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (c1 . b1) * (c2 . b2) ) by POLYNOM1:def 10;
A5: dom s = Seg (len (decomp b)) by A3, FINSEQ_1:def 3
.= dom (decomp b) by FINSEQ_1:def 3 ;

A6: now :: thesis: for k being Element of NAT st k in dom s holds
s /. k = 0. L

let k be Element of NAT ; :: thesis: ( k in dom s implies s /. k = 0. L )
assume A7: k in dom s ; :: thesis: s /. k = 0. L
then consider b1, b2 being bag of n such that
A8: (decomp b) /. k = <*b1,b2*> and
A9: s /. k = (c1 . b1) * (c2 . b2) by A4;
consider b19, b29 being bag of n such that
A10: (decomp b) /. k = <*b19,b29*> and
A11: b = b19 + b29 by A5, A7, PRE_POLY:68;
A12: b2 = <*b19,b29*> . 2 by A8, A10
.= b29 ;
b1 = <*b19,b29*> . 1 by A8, A10
.= b19 ;
then A13: ( b1 <> EmptyBag n or b2 <> EmptyBag n ) by A1, A11, A12, PRE_POLY:53;

now :: thesis: ( ( c1 . b1 = 0. L & s /. k = 0. L ) or ( c2 . b2 = 0. L & s /. k = 0. L ) )

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

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

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

end;

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

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

end;

end;

end;

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

end;

now :: thesis: ( ( dom s = {} & (c1 *' c2) . b = 0. L ) or ( dom s <> {} & (c1 *' c2) . b = 0. L ) )

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:41;
hence (c1 *' c2) . b = 0. L by A3; :: thesis: verum

end;

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

set k = the Element of dom s;
A15: the Element of dom s in dom s by A14;
for k9 being Element of NAT st k9 in dom s & k9 <> the Element of dom s holds
s /. k9 = 0. L by A6;
then Sum s = s /. the Element of dom s by A15, POLYNOM2:3;
hence (c1 *' c2) . b = 0. L by A2, A6, A15; :: thesis: verum

end;

end;

end;

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

end;

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