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 st Support m = {b} ) by Th6;

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

then A3: term m = EmptyBag X by Def6;
A4: m = 0_ X,L by A2, Th1;
set m' = Monom (coefficient m),(term m);

A5: now

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

end;

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

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 x' = x as Element of Bags X ;

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

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

end;

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

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

A19: 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 A20: u = b by TARSKI:def 1;
( (Monom (coefficient m),(term m)) . b <> 0. L & b is Element of Bags X ) by A13, A18, POLYNOM1:def 9;
hence u in Support (Monom (coefficient m),(term m)) by A20, POLYNOM1:def 9; :: thesis: verum

end;

now

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

now

assume A22: u <> b ; :: thesis: (Monom (coefficient m),(term m)) . u' = 0. L
A23: b in dom (0_ X,L) by A15, POLYNOM1:def 14;
dom (b .--> (m . b)) = {b} by FUNCOP_1:19;
then A24: not u' in dom (b .--> (m . b)) by A22, TARSKI:def 1;
(Monom (coefficient m),(term m)) . u' = ((0_ X,L) +* (b .--> (m . b))) . u' by A14, A23, FUNCT_7:def 3
.= (0_ X,L) . u' by A24, FUNCT_4:12 ;
hence (Monom (coefficient m),(term m)) . u' = 0. L by POLYNOM1:81; :: thesis: verum

end;

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

end;

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

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 x' = x as Element of Bags X ;

now

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

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

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

end;

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

then A27: not x in Support m by A12, TARSKI:def 1;
A28: not x in Support (Monom (coefficient m),(term m)) by A25, A26, TARSKI:def 1;
thus m . x' = 0. L by A27, POLYNOM1:def 9
.= (Monom (coefficient m),(term m)) . x' by A28, POLYNOM1:def 9 ; :: 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:9; :: thesis: verum

end;

end;