let X be set ; :: thesis: for L being non empty ZeroStr
for m being Monomial of X,L holds Monom ((),(term m)) = m

let L be non empty ZeroStr ; :: thesis: for m being Monomial of X,L holds Monom ((),(term m)) = m
let m be Monomial of X,L; :: thesis: Monom ((),(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 ((),(term m)) = m
A4: m = 0_ (X,L) by ;
set m9 = Monom ((),(term m));
A5: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 8
.= Bags X ;
A6: EmptyBag X in dom (() .--> (0. L)) by TARSKI:def 1;
A7: term m = EmptyBag X by ;
then A8: (Monom ((),(term m))) . () = ((0_ (X,L)) +* (() .--> (0. L))) . () by
.= (() .--> (0. L)) . () by
.= 0. L by FUNCOP_1:72 ;
now :: thesis: for x being object st x in Bags X holds
m . x = (Monom ((),(term m))) . x
let x be object ; :: thesis: ( x in Bags X implies m . x = (Monom ((),(term m))) . x )
assume x in Bags X ; :: thesis: m . x = (Monom ((),(term m))) . x
then reconsider x9 = x as Element of Bags X ;
now :: thesis: ( ( x9 = EmptyBag X & (Monom ((),(term m))) . x9 = 0. L ) or ( x <> EmptyBag X & (Monom ((),(term m))) . x9 = 0. L ) )
per cases ( x9 = EmptyBag X or x <> EmptyBag X ) ;
case x9 = EmptyBag X ; :: thesis: (Monom ((),(term m))) . x9 = 0. L
hence (Monom ((),(term m))) . x9 = 0. L by A8; :: thesis: verum
end;
case x <> EmptyBag X ; :: thesis: (Monom ((),(term m))) . x9 = 0. L
then A9: not x9 in dom (() .--> (0. L)) by TARSKI:def 1;
(Monom ((),(term m))) . x9 = ((0_ (X,L)) +* (() .--> (0. L))) . x9 by
.= (0_ (X,L)) . x9 by ;
hence (Monom ((),(term m))) . x9 = 0. L by POLYNOM1:22; :: thesis: verum
end;
end;
end;
hence m . x = (Monom ((),(term m))) . x by ; :: thesis: verum
end;
hence Monom ((),(term m)) = m ; :: thesis: verum
end;
suppose ex b being bag of X st Support m = {b} ; :: thesis: Monom ((),(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 ((),(term m));
A12: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 8
.= Bags X ;
A13: b in Support m by ;
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 ((),(term m))) holds
u in {b}
let u be object ; :: thesis: ( u in Support (Monom ((),(term m))) implies u in {b} )
assume A16: u in Support (Monom ((),(term m))) ; :: thesis: u in {b}
then reconsider u9 = u as Element of Bags X ;
now :: thesis: ( u <> b implies (Monom ((),(term m))) . u9 = 0. L )
assume u <> b ; :: thesis: (Monom ((),(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 ;
then (Monom ((),(term m))) . u9 = ((0_ (X,L)) +* (b .--> (m . b))) . u9 by
.= (0_ (X,L)) . u9 by ;
hence (Monom ((),(term m))) . u9 = 0. L by POLYNOM1:22; :: thesis: verum
end;
hence u in {b} by ; :: thesis: verum
end;
b in Bags X by PRE_POLY:def 12;
then A18: (Monom ((),(term m))) . b = ((0_ (X,L)) +* (b .--> (m . b))) . b by
.= (b .--> (m . b)) . b by
.= m . b by FUNCOP_1:72 ;
now :: thesis: for u being object st u in {b} holds
u in Support (Monom ((),(term m)))
let u be object ; :: thesis: ( u in {b} implies u in Support (Monom ((),(term m))) )
assume u in {b} ; :: thesis: u in Support (Monom ((),(term m)))
then A19: u = b by TARSKI:def 1;
(Monom ((),(term m))) . b <> 0. L by ;
hence u in Support (Monom ((),(term m))) by ; :: thesis: verum
end;
then A20: Support (Monom ((),(term m))) = {b} by ;
now :: thesis: for x being object st x in Bags X holds
m . x = (Monom ((),(term m))) . x
let x be object ; :: thesis: ( x in Bags X implies m . x = (Monom ((),(term m))) . x )
assume x in Bags X ; :: thesis: m . x = (Monom ((),(term m))) . x
then reconsider x9 = x as Element of Bags X ;
now :: thesis: ( ( x = b & (Monom ((),(term m))) . x9 = m . x9 ) or ( x <> b & m . x9 = (Monom ((),(term m))) . x9 ) )
per cases ( x = b or x <> b ) ;
case x = b ; :: thesis: (Monom ((),(term m))) . x9 = m . x9
hence (Monom ((),(term m))) . x9 = m . x9 by A18; :: thesis: verum
end;
case A21: x <> b ; :: thesis: m . x9 = (Monom ((),(term m))) . x9
then A22: not x in Support (Monom ((),(term m))) by ;
not x in Support m by ;
hence m . x9 = 0. L by POLYNOM1:def 4
.= (Monom ((),(term m))) . x9 by ;
:: thesis: verum
end;
end;
end;
hence m . x = (Monom ((),(term m))) . x ; :: thesis: verum
end;
hence Monom ((),(term m)) = m ; :: thesis: verum
end;
end;