per cases ( Support (m1 *' m2) = {} or Support (m1 *' m2) <> {} ) ;

suppose Support (m1 *' m2) = {} ; :: thesis: m1 *' m2 is monomial-like

hence m1 *' m2 is monomial-like by POLYNOM7:6; :: thesis: verum

end;

suppose A1: Support (m1 *' m2) <> {} ; :: thesis: m1 *' m2 is monomial-like

now :: thesis: ( ( Support m1 <> {} & Support m2 <> {} & m1 *' m2 is monomial-like ) or ( ( Support m1 = {} or Support m2 = {} ) & m1 *' m2 is monomial-like ) )

per cases ( ( Support m1 <> {} & Support m2 <> {} ) or Support m1 = {} or Support m2 = {} ) ;

case A2: ( Support m1 <> {} & Support m2 <> {} ) ; :: thesis: m1 *' m2 is monomial-like

then consider mb2 being bag of n such that
A3: Support m2 = {mb2} by POLYNOM7:6;
mb2 in Support m2 by A3, TARSKI:def 1;
then A4: m2 . mb2 <> 0. L by POLYNOM1:def 4;

A5: now :: thesis: for b being bag of n st b <> mb2 holds
m2 . b = 0. L

let b be bag of n; :: thesis: ( b <> mb2 implies m2 . b = 0. L )
assume A6: b <> mb2 ; :: thesis: m2 . b = 0. L
consider b9 being bag of n such that
A7: for b being bag of n st b <> b9 holds
m2 . b = 0. L by POLYNOM7:def 3;
b9 = mb2 by A4, A7;
hence m2 . b = 0. L by A6, A7; :: thesis: verum

end;

consider mb1 being bag of n such that
A8: Support m1 = {mb1} by A2, POLYNOM7:6;
mb1 in Support m1 by A8, TARSKI:def 1;
then A9: m1 . mb1 <> 0. L by POLYNOM1:def 4;

A10: now :: thesis: for b being bag of n st b <> mb1 holds
m1 . b = 0. L

let b be bag of n; :: thesis: ( b <> mb1 implies m1 . b = 0. L )
assume A11: b <> mb1 ; :: thesis: m1 . b = 0. L
consider b9 being bag of n such that
A12: for b being bag of n st b <> b9 holds
m1 . b = 0. L by POLYNOM7:def 3;
b9 = mb1 by A9, A12;
hence m1 . b = 0. L by A11, A12; :: thesis: verum

end;

set b = the Element of Support (m1 *' m2);
A13: the Element of Support (m1 *' m2) in Support (m1 *' m2) by A1;
then the Element of Support (m1 *' m2) is Element of Bags n ;
then reconsider b = the Element of Support (m1 *' m2) as bag of n ;
consider s being FinSequence of L such that
A14: (m1 *' m2) . b = Sum s and
A15: len s = len (decomp b) and
A16: 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 = (m1 . b1) * (m2 . b2) ) by POLYNOM1:def 10;
A17: dom s = Seg (len (decomp b)) by A15, FINSEQ_1:def 3
.= dom (decomp b) by FINSEQ_1:def 3 ;

A18: now :: thesis: not b <> mb1 + mb2

assume A19: b <> mb1 + mb2 ; :: thesis: contradiction

A20: 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 A21: k in dom s ; :: thesis: s /. k = 0. L
then consider b1, b2 being bag of n such that
A22: (decomp b) /. k = <*b1,b2*> and
A23: s /. k = (m1 . b1) * (m2 . b2) by A16;
consider b19, b29 being bag of n such that
A24: (decomp b) /. k = <*b19,b29*> and
A25: b = b19 + b29 by A17, A21, PRE_POLY:68;
A26: b2 = <*b19,b29*> . 2 by A22, A24
.= b29 ;
A27: b1 = <*b19,b29*> . 1 by A22, A24
.= b19 ;

now :: thesis: ( ( b1 <> mb1 & (m1 . b1) * (m2 . b2) = 0. L ) or ( b2 <> mb2 & (m1 . b1) * (m2 . b2) = 0. L ) )

per cases ( b1 <> mb1 or b2 <> mb2 ) by A19, A25, A27, A26;

case b1 <> mb1 ; :: thesis: (m1 . b1) * (m2 . b2) = 0. L

then m1 . b1 = 0. L by A10;
hence (m1 . b1) * (m2 . b2) = 0. L ; :: thesis: verum

end;

case b2 <> mb2 ; :: thesis: (m1 . b1) * (m2 . b2) = 0. L

then m2 . b2 = 0. L by A5;
hence (m1 . b1) * (m2 . b2) = 0. L ; :: thesis: verum

end;

end;

end;

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

end;

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

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

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

then s = <*> the carrier of L by RELAT_1:41;
hence (m1 *' m2) . b = 0. L by A15; :: thesis: verum

end;

case A28: dom s <> {} ; :: thesis: (m1 *' m2) . b = 0. L

set k = the Element of dom s;
A29: the Element of dom s in dom s by A28;
for k9 being Element of NAT st k9 in dom s & k9 <> the Element of dom s holds
s /. k9 = 0. L by A20;
then s /. the Element of dom s = (m1 *' m2) . b by A14, A29, POLYNOM2:3;
hence (m1 *' m2) . b = 0. L by A20, A29; :: thesis: verum

end;

end;

end;

hence contradiction by A13, POLYNOM1:def 4; :: thesis: verum

end;

now :: thesis: for b9 being bag of n st b9 <> b holds
(m1 *' m2) . b9 = 0. L

let b9 be bag of n; :: thesis: ( b9 <> b implies (m1 *' m2) . b9 = 0. L )
assume A30: b9 <> b ; :: thesis: (m1 *' m2) . b9 = 0. L
consider s being FinSequence of L such that
A31: (m1 *' m2) . b9 = Sum s and
A32: len s = len (decomp b9) and
A33: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b9) /. k = <*b1,b2*> & s /. k = (m1 . b1) * (m2 . b2) ) by POLYNOM1:def 10;
A34: dom s = Seg (len (decomp b9)) by A32, FINSEQ_1:def 3
.= dom (decomp b9) by FINSEQ_1:def 3 ;

A35: 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 A36: k in dom s ; :: thesis: s /. k = 0. L
then consider b1, b2 being bag of n such that
A37: (decomp b9) /. k = <*b1,b2*> and
A38: s /. k = (m1 . b1) * (m2 . b2) by A33;
consider b19, b29 being bag of n such that
A39: (decomp b9) /. k = <*b19,b29*> and
A40: b9 = b19 + b29 by A34, A36, PRE_POLY:68;
A41: b2 = <*b19,b29*> . 2 by A37, A39
.= b29 ;
A42: b1 = <*b19,b29*> . 1 by A37, A39
.= b19 ;

now :: thesis: ( ( b1 <> mb1 & (m1 . b1) * (m2 . b2) = 0. L ) or ( b2 <> mb2 & (m1 . b1) * (m2 . b2) = 0. L ) )

per cases ( b1 <> mb1 or b2 <> mb2 ) by A18, A30, A40, A42, A41;

case b1 <> mb1 ; :: thesis: (m1 . b1) * (m2 . b2) = 0. L

then m1 . b1 = 0. L by A10;
hence (m1 . b1) * (m2 . b2) = 0. L ; :: thesis: verum

end;

case b2 <> mb2 ; :: thesis: (m1 . b1) * (m2 . b2) = 0. L

then m2 . b2 = 0. L by A5;
hence (m1 . b1) * (m2 . b2) = 0. L ; :: thesis: verum

end;

end;

end;

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

end;

now :: thesis: ( ( dom s = {} & (m1 *' m2) . b9 = 0. L ) or ( dom s <> {} & (m1 *' m2) . b9 = 0. L ) )

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

case dom s = {} ; :: thesis: (m1 *' m2) . b9 = 0. L

then s = <*> the carrier of L by RELAT_1:41;
hence (m1 *' m2) . b9 = 0. L by A32; :: thesis: verum

end;

case A43: dom s <> {} ; :: thesis: (m1 *' m2) . b9 = 0. L

set k = the Element of dom s;
A44: the Element of dom s in dom s by A43;
for k9 being Element of NAT st k9 in dom s & k9 <> the Element of dom s holds
s /. k9 = 0. L by A35;
then s /. the Element of dom s = (m1 *' m2) . b9 by A31, A44, POLYNOM2:3;
hence (m1 *' m2) . b9 = 0. L by A35, A44; :: thesis: verum

end;

end;

end;

hence (m1 *' m2) . b9 = 0. L ; :: thesis: verum

end;

hence m1 *' m2 is monomial-like by POLYNOM7:def 3; :: thesis: verum

end;

case A45: ( Support m1 = {} or Support m2 = {} ) ; :: thesis: m1 *' m2 is monomial-like

now :: thesis: ( ( Support m1 = {} & m1 *' m2 is monomial-like ) or ( Support m2 = {} & m1 *' m2 is monomial-like ) )

per cases ( Support m1 = {} or Support m2 = {} ) by A45;

case Support m1 = {} ; :: thesis: m1 *' m2 is monomial-like

then m1 = 0_ (n,L) by POLYNOM7:1;
hence m1 *' m2 is monomial-like by Th2; :: thesis: verum

end;

case Support m2 = {} ; :: thesis: m1 *' m2 is monomial-like

then m2 = 0_ (n,L) by POLYNOM7:1;
hence m1 *' m2 is monomial-like by POLYNOM1:28; :: thesis: verum

end;

end;

end;

hence m1 *' m2 is monomial-like ; :: thesis: verum

end;

end;

end;

hence m1 *' m2 is monomial-like ; :: thesis: verum

end;

end;