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

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

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

A2: now :: thesis: not coefficient m <> 0. L

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

end;

A4: m = 0_ (X,L) by A1, Th1;
set m9 = Monom ((coefficient m),(term m));
A5: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 8
.= Bags X ;
A6: EmptyBag X in dom ((EmptyBag X) .--> (0. L)) by TARSKI:def 1;
A7: term m = EmptyBag X by A1, Def5;
then A8: (Monom ((coefficient m),(term m))) . (EmptyBag X) = ((0_ (X,L)) +* ((EmptyBag X) .--> (0. L))) . (EmptyBag X) by A2, A5, FUNCT_7:def 3
.= ((EmptyBag X) .--> (0. L)) . (EmptyBag X) by A6, FUNCT_4:13
.= 0. L by FUNCOP_1:72 ;

now :: thesis: for x being object st x in Bags X holds
m . x = (Monom ((coefficient m),(term m))) . x

let x be object ; :: 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 :: thesis: ( ( x9 = EmptyBag X & (Monom ((coefficient m),(term m))) . x9 = 0. L ) or ( x <> EmptyBag X & (Monom ((coefficient m),(term m))) . x9 = 0. L ) )

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 A8; :: thesis: verum

end;

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

then A9: not x9 in dom ((EmptyBag X) .--> (0. L)) by TARSKI:def 1;
(Monom ((coefficient m),(term m))) . x9 = ((0_ (X,L)) +* ((EmptyBag X) .--> (0. L))) . x9 by A7, A2, A5, FUNCT_7:def 3
.= (0_ (X,L)) . x9 by A9, 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 A4, POLYNOM1:22; :: thesis: verum

end;

hence Monom ((coefficient m),(term m)) = m ; :: 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
A10: Support m = {b} ;
set a = m . b;
A11: b in dom (b .--> (m . b)) by TARSKI:def 1;
set m9 = Monom ((coefficient m),(term m));
A12: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 8
.= Bags X ;
A13: b in Support m by A10, TARSKI:def 1;
then m . b <> 0. L by POLYNOM1:def 4;
then A14: term m = b by Def5;

A15: now :: thesis: for u being object st u in Support (Monom ((coefficient m),(term m))) holds
u in {b}

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

now :: thesis: ( u <> b implies (Monom ((coefficient m),(term m))) . u9 = 0. L )

assume u <> b ; :: thesis: (Monom ((coefficient m),(term m))) . u9 = 0. L
then A17: not u9 in dom (b .--> (m . b)) by TARSKI:def 1;
b in dom (0_ (X,L)) by A12, PRE_POLY:def 12;
then (Monom ((coefficient m),(term m))) . u9 = ((0_ (X,L)) +* (b .--> (m . b))) . u9 by A14, FUNCT_7:def 3
.= (0_ (X,L)) . u9 by A17, FUNCT_4:11 ;
hence (Monom ((coefficient m),(term m))) . u9 = 0. L by POLYNOM1:22; :: thesis: verum

end;

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

end;

b in Bags X by PRE_POLY:def 12;
then A18: (Monom ((coefficient m),(term m))) . b = ((0_ (X,L)) +* (b .--> (m . b))) . b by A14, A12, FUNCT_7:def 3
.= (b .--> (m . b)) . b by A11, FUNCT_4:13
.= m . b by FUNCOP_1:72 ;

now :: thesis: for u being object st u in {b} holds
u in Support (Monom ((coefficient m),(term m)))

let u be object ; :: 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 A19: u = b by TARSKI:def 1;
(Monom ((coefficient m),(term m))) . b <> 0. L by A13, A18, POLYNOM1:def 4;
hence u in Support (Monom ((coefficient m),(term m))) by A13, A19, POLYNOM1:def 4; :: thesis: verum

end;

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

now :: thesis: for x being object st x in Bags X holds
m . x = (Monom ((coefficient m),(term m))) . x

let x be object ; :: 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 :: thesis: ( ( x = b & (Monom ((coefficient m),(term m))) . x9 = m . x9 ) or ( x <> b & m . x9 = (Monom ((coefficient m),(term m))) . x9 ) )

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 A18; :: thesis: verum

end;

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

then A22: not x in Support (Monom ((coefficient m),(term m))) by A20, TARSKI:def 1;
not x in Support m by A10, A21, TARSKI:def 1;
hence m . x9 = 0. L by POLYNOM1:def 4
.= (Monom ((coefficient m),(term m))) . x9 by A22, POLYNOM1:def 4 ;
:: thesis: verum

end;

end;

end;

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

end;

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

end;

end;