set p = a * m;

now :: thesis: ( ( Support m = {} & a * m is monomial-like ) or ( ex b being bag of X st Support m = {b} & a * m is monomial-like ) )

per cases ( Support m = {} or ex b being bag of X st Support m = {b} ) by POLYNOM7:6;

case A1: Support m = {} ; :: thesis: a * m is monomial-like

now :: thesis: not Support (a * m) <> {}

set b = the Element of Support (a * m);
assume A2: Support (a * m) <> {} ; :: thesis: contradiction
then the Element of Support (a * m) in Support (a * m) ;
then reconsider b = the Element of Support (a * m) as Element of Bags X ;
(a * m) . b = a * (m . b) by POLYNOM7:def 9
.= a * (0. L) by A1, POLYNOM1:def 4
.= 0. L by BINOM:2 ;
hence contradiction by A2, POLYNOM1:def 4; :: thesis: verum

end;

hence a * m is monomial-like by POLYNOM7:6; :: thesis: verum

end;

case ex b being bag of X st Support m = {b} ; :: thesis: a * m is monomial-like

then consider b being bag of X such that
A3: Support m = {b} ;
reconsider b = b as Element of Bags X by PRE_POLY:def 12;

now :: thesis: ( ( a = 0. L & Support (a * m) = {} ) or ( a <> 0. L & a * m is monomial-like ) )

per cases ( a = 0. L or a <> 0. L ) ;

case A4: a = 0. L ; :: thesis: Support (a * m) = {}

now :: thesis: not Support (a * m) <> {}

set b = the Element of Support (a * m);
assume A5: Support (a * m) <> {} ; :: thesis: contradiction
then the Element of Support (a * m) in Support (a * m) ;
then reconsider b = the Element of Support (a * m) as Element of Bags X ;
(a * m) . b = a * (m . b) by POLYNOM7:def 9
.= 0. L by A4, BINOM:1 ;
hence contradiction by A5, POLYNOM1:def 4; :: thesis: verum

end;

hence Support (a * m) = {} ; :: thesis: verum

end;

case a <> 0. L ; :: thesis: a * m is monomial-like

A6: now :: thesis: for b9 being Element of Bags X st b9 <> b holds
(a * m) . b9 = 0. L

let b9 be Element of Bags X; :: thesis: ( b9 <> b implies (a * m) . b9 = 0. L )
assume b9 <> b ; :: thesis: (a * m) . b9 = 0. L
then not b9 in Support m by A3, TARSKI:def 1;
then A7: m . b9 = 0. L by POLYNOM1:def 4;
(a * m) . b9 = a * (m . b9) by POLYNOM7:def 9;
hence (a * m) . b9 = 0. L by A7, BINOM:2; :: thesis: verum

end;

now :: thesis: ( ( a * (m . b) = 0. L & Support (a * m) = {} ) or ( a * (m . b) <> 0. L & Support (a * m) = {b} ) )

per cases ( a * (m . b) = 0. L or a * (m . b) <> 0. L ) ;

case A8: a * (m . b) = 0. L ; :: thesis: Support (a * m) = {}

now :: thesis: not Support (a * m) <> {}

set b9 = the Element of Support (a * m);
assume A9: Support (a * m) <> {} ; :: thesis: contradiction
then the Element of Support (a * m) in Support (a * m) ;
then reconsider b9 = the Element of Support (a * m) as Element of Bags X ;
A10: (a * m) . b9 <> 0. L by A9, POLYNOM1:def 4;
then b9 = b by A6;
hence contradiction by A8, A10, POLYNOM7:def 9; :: thesis: verum

end;

hence Support (a * m) = {} ; :: thesis: verum

end;

case A11: a * (m . b) <> 0. L ; :: thesis: Support (a * m) = {b}

A12: now :: thesis: for u being object st u in Support (a * m) holds
u in {b}

let u be object ; :: thesis: ( u in Support (a * m) implies u in {b} )
assume A13: u in Support (a * m) ; :: thesis: u in {b}
then reconsider u9 = u as Element of Bags X ;
(a * m) . u9 <> 0. L by A13, POLYNOM1:def 4;
then u9 = b by A6;
hence u in {b} by TARSKI:def 1; :: thesis: verum

end;

now :: thesis: for u being object st u in {b} holds
u in Support (a * m)

let u be object ; :: thesis: ( u in {b} implies u in Support (a * m) )
assume u in {b} ; :: thesis: u in Support (a * m)
then A14: u = b by TARSKI:def 1;
(a * m) . b <> 0. L by A11, POLYNOM7:def 9;
hence u in Support (a * m) by A14, POLYNOM1:def 4; :: thesis: verum

end;

hence Support (a * m) = {b} by A12, TARSKI:2; :: thesis: verum

end;

end;

end;

hence a * m is monomial-like by POLYNOM7:6; :: thesis: verum

end;

end;

end;

hence a * m is monomial-like by POLYNOM7:6; :: thesis: verum

end;

end;

end;

hence a * m is monomial-like ; :: thesis: verum