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

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

suppose A2: Support m = {} ; :: thesis: Monom ((coefficient m),(term m)) = m

A3: now

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

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 7
.= Bags X by FUNCOP_1:13 ;
A7: dom ((EmptyBag X) .--> (0. L)) = {(EmptyBag X)} by FUNCOP_1:13;
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:13
.= 0. L by FUNCOP_1:72 ;

now

let x be set ; :: thesis: ( x in Bags X implies m . x = (Monom ((coefficient m),(term m))) . x )
assume x in Bags X ; :: thesis: m . x = (Monom ((coefficient m),(term m))) . x
then reconsider x9 = x as Element of Bags X ;

now

per cases ( x9 = EmptyBag X or x <> EmptyBag X ) ;

case x9 = EmptyBag X ; :: thesis: (Monom ((coefficient m),(term m))) . x9 = 0. L

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

end;

case x <> EmptyBag X ; :: thesis: (Monom ((coefficient m),(term m))) . x9 = 0. L

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:11 ;
hence (Monom ((coefficient m),(term m))) . x9 = 0. L by POLYNOM1:22; :: thesis: verum

end;

end;

end;

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

end;

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

end;

suppose ex b being bag of X st Support m = {b} ; :: thesis: Monom ((coefficient m),(term m)) = m

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:13;
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 7
.= Bags X by FUNCOP_1:13 ;
A15: b in Support m by A12, TARSKI:def 1;
then m . b <> 0. L by POLYNOM1:def 3;
then A16: term m = b by Def6;

A17: now

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

now

A19: dom (b .--> (m . b)) = {b} by FUNCOP_1:13;
assume u <> b ; :: thesis: (Monom ((coefficient m),(term m))) . u9 = 0. L
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:11 ;
hence (Monom ((coefficient m),(term m))) . u9 = 0. L by POLYNOM1:22; :: thesis: verum

end;

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

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:13
.= m . b by FUNCOP_1:72 ;

now

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

end;

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

now

let x be set ; :: thesis: ( x in Bags X implies m . x = (Monom ((coefficient m),(term m))) . x )
assume x in Bags X ; :: thesis: m . x = (Monom ((coefficient m),(term m))) . x
then reconsider x9 = x as Element of Bags X ;

now

per cases ( x = b or x <> b ) ;

case x = b ; :: thesis: (Monom ((coefficient m),(term m))) . x9 = m . x9

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

end;

case A24: x <> b ; :: thesis: m . x9 = (Monom ((coefficient m),(term m))) . x9

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 3
.= (Monom ((coefficient m),(term m))) . x9 by A25, POLYNOM1:def 3 ;
:: thesis: verum

end;

end;

end;

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

end;

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

end;

end;