let X be set ; :: thesis:
let L be non empty ZeroStr ; :: thesis:
let m be Monomial of X,L; :: thesis:
A1: ( dom m = Bags X & dom (Monom (coefficient m),(term m)) = Bags X ) by FUNCT_2:def 1;

per cases by Th6;

suppose A2: Support m = {} ; :: thesis:

A3: now

A4: term m is Element of Bags X by PRE_POLY:def 12;
assume coefficient m <> 0. L ; :: thesis:
hence contradiction by A2, A4, POLYNOM1:def 9; :: thesis:

end;

A5: m = 0_ X,L by A2, Th1;
set m9 = Monom (coefficient m),(term m);
A6: dom (0_ X,L) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19 ;
A7: dom ((EmptyBag X) .--> (0. L)) = {(EmptyBag X)} by FUNCOP_1:19;
then A8: EmptyBag X in dom ((EmptyBag X) .--> (0. L)) by TARSKI:def 1;
A9: term m = EmptyBag X by A2, Def6;
then A10: (Monom (coefficient m),(term m)) . (EmptyBag X) = ((0_ X,L) +* ((EmptyBag X) .--> (0. L))) . (EmptyBag X) by A3, A6, FUNCT_7:def 3
.= ((EmptyBag X) .--> (0. L)) . (EmptyBag X) by A8, FUNCT_4:14
.= 0. L by FUNCOP_1:87 ;

now

let x be set ; :: thesis:
assume x in Bags X ; :: thesis:
then reconsider x9 = x as Element of Bags X ;

now

per cases ;

case x9 = EmptyBag X ; :: thesis:

hence (Monom (coefficient m),(term m)) . x9 = 0. L by A10; :: thesis:

end;

case x <> EmptyBag X ; :: thesis:

then A11: not x9 in dom ((EmptyBag X) .--> (0. L)) by A7, TARSKI:def 1;
(Monom (coefficient m),(term m)) . x9 = ((0_ X,L) +* ((EmptyBag X) .--> (0. L))) . x9 by A9, A3, A6, FUNCT_7:def 3
.= (0_ X,L) . x9 by A11, FUNCT_4:12 ;
hence (Monom (coefficient m),(term m)) . x9 = 0. L by POLYNOM1:81; :: thesis:

end;

end;

end;

hence m . x = (Monom (coefficient m),(term m)) . x by A5, POLYNOM1:81; :: thesis:

end;

hence Monom (coefficient m),(term m) = m by A1, FUNCT_1:9; :: thesis:

end;

suppose ex b being bag of X st Support m = {b} ; :: thesis:

then consider b being bag of X such that
A12: Support m = {b} ;
set a = m . b;
dom (b .--> (m . b)) = {b} by FUNCOP_1:19;
then A13: b in dom (b .--> (m . b)) by TARSKI:def 1;
set m9 = Monom (coefficient m),(term m);
A14: dom (0_ X,L) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19 ;
A15: b in Support m by A12, TARSKI:def 1;
then m . b <> 0. L by POLYNOM1:def 9;
then A16: term m = b by Def6;

A17: now

let u be set ; :: thesis:
assume A18: u in Support (Monom (coefficient m),(term m)) ; :: thesis:
then reconsider u9 = u as Element of Bags X ;

now

A19: dom (b .--> (m . b)) = {b} by FUNCOP_1:19;
assume u <> b ; :: thesis:
then A20: not u9 in dom (b .--> (m . b)) by A19, TARSKI:def 1;
b in dom (0_ X,L) by A14, PRE_POLY:def 12;
then (Monom (coefficient m),(term m)) . u9 = ((0_ X,L) +* (b .--> (m . b))) . u9 by A16, FUNCT_7:def 3
.= (0_ X,L) . u9 by A20, FUNCT_4:12 ;
hence (Monom (coefficient m),(term m)) . u9 = 0. L by POLYNOM1:81; :: thesis:

end;

hence u in {b} by A18, POLYNOM1:def 9, TARSKI:def 1; :: thesis:

end;

b in Bags X by PRE_POLY:def 12;
then A21: (Monom (coefficient m),(term m)) . b = ((0_ X,L) +* (b .--> (m . b))) . b by A16, A14, FUNCT_7:def 3
.= (b .--> (m . b)) . b by A13, FUNCT_4:14
.= m . b by FUNCOP_1:87 ;

now

let u be set ; :: thesis:
assume u in {b} ; :: thesis:
then A22: u = b by TARSKI:def 1;
(Monom (coefficient m),(term m)) . b <> 0. L by A15, A21, POLYNOM1:def 9;
hence u in Support (Monom (coefficient m),(term m)) by A15, A22, POLYNOM1:def 9; :: thesis:

end;

then A23: Support (Monom (coefficient m),(term m)) = {b} by A17, TARSKI:2;

now

let x be set ; :: thesis:
assume x in Bags X ; :: thesis:
then reconsider x9 = x as Element of Bags X ;

now

per cases ;

case x = b ; :: thesis:

hence (Monom (coefficient m),(term m)) . x9 = m . x9 by A21; :: thesis:

end;

case A24: x <> b ; :: thesis:

then A25: not x in Support (Monom (coefficient m),(term m)) by A23, TARSKI:def 1;
not x in Support m by A12, A24, TARSKI:def 1;
hence m . x9 = 0. L by POLYNOM1:def 9
.= (Monom (coefficient m),(term m)) . x9 by A25, POLYNOM1:def 9 ;
:: thesis:

end;

end;

end;

hence m . x = (Monom (coefficient m),(term m)) . x ; :: thesis:

end;

hence Monom (coefficient m),(term m) = m by A1, FUNCT_1:9; :: thesis:

end;

end;