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

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;

end;

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

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 ;

end;

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

A4:
m = 0_ (X,L)
by A1, Th1;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;assume coefficient m <> 0. L ; :: thesis: contradiction

hence contradiction by A1, A3, POLYNOM1:def 4; :: thesis: verum

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

hence
Monom ((coefficient m),(term m)) = m
; :: thesis: verumm . 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 ;

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

hence
m . x = (Monom ((coefficient m),(term m))) . x
by A4, POLYNOM1:22; :: thesis: verumper cases
( x9 = EmptyBag X or x <> EmptyBag X )
;

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

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;

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 ;

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

b in Bags X
by PRE_POLY:def 12;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 ;

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

hence
u in {b}
by A16, POLYNOM1:def 4, TARSKI:def 1; :: thesis: verumassume
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;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

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

then A20:
Support (Monom ((coefficient m),(term m))) = {b}
by A15, TARSKI:2;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;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

now :: thesis: for x being object st x in Bags X holds

m . x = (Monom ((coefficient m),(term m))) . x

hence
Monom ((coefficient m),(term m)) = m
; :: thesis: verumm . 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 ;

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

hence
m . x = (Monom ((coefficient m),(term m))) . x
; :: thesis: verumper cases
( x = b or x <> b )
;

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