set p = a * m;

now

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

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

now

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

end;

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

end;

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

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

now

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

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

now

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

end;

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

end;

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

A6: now

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

end;

now

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

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

end;

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

end;

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

A12: now

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

end;

now

let u be set ; :: thesis: ( u in Support (a * m) implies u in {b} )
assume A14: u in Support (a * m) ; :: thesis: u in {b}
then reconsider u' = u as Element of Bags X ;
(a * m) . u' <> 0. L by A14, POLYNOM1:def 9;
then u' = b by A6;
hence u in {b} by TARSKI:def 1; :: 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