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 ) )end;

hence
a * m is monomial-like
; :: thesis: verumper cases
( Support m = {} or ex b being bag of X st Support m = {b} )
by POLYNOM7:6;

end;

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

end;

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

hence
a * m is monomial-like
by POLYNOM7:6; :: thesis: verumset 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;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

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;

end;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 ) )end;

hence
a * m is monomial-like
by POLYNOM7:6; :: thesis: verumper cases
( a = 0. L or a <> 0. L )
;

end;

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

end;

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

hence
Support (a * m) = {}
; :: thesis: verumset 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;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

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

end;

A6: now :: thesis: for b9 being Element of Bags X st b9 <> b holds

(a * m) . b9 = 0. L

(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;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

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

hence
a * m is monomial-like
by POLYNOM7:6; :: thesis: verumper cases
( a * (m . b) = 0. L or a * (m . b) <> 0. L )
;

end;

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

end;

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

hence
Support (a * m) = {}
; :: thesis: verumset 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;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

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

end;

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

u in {b}

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;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

now :: thesis: for u being object st u in {b} holds

u in Support (a * m)

hence
Support (a * m) = {b}
by A12, TARSKI:2; :: thesis: verumu 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;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