let n be Ordinal; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr
for p being Polynomial of n,L
for m being non-zero Monomial of n,L holds card (Support p) = card (Support (m *' p))
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of n,L
for m being non-zero Monomial of n,L holds card (Support p) = card (Support (m *' p))
let p be Polynomial of n,L; :: thesis: for m being non-zero Monomial of n,L holds card (Support p) = card (Support (m *' p))
let m be non-zero Monomial of n,L; :: thesis: card (Support p) = card (Support (m *' p))
defpred S₁[ object , object ] means $2 = (term m) + (In ($1,(Bags n)));
set T = the connected admissible TermOrder of n;
m <> 0_ (n,L) by POLYNOM7:def 1;
then Support m <> {} by POLYNOM7:1;
then A1: Support m = {(term m)} by POLYNOM7:7;
A2: for x being object st x in Support p holds
ex y being object st
( y in Support (m *' p) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Support p implies ex y being object st
( y in Support (m *' p) & S₁[x,y] ) )
assume A3: x in Support p ; :: thesis: ex y being object st
( y in Support (m *' p) & S₁[x,y] )
then reconsider x9 = x as Element of Bags n ;
(term m) + x9 in Support (m *' p) by A3, Th8;
hence ex y being object st
( y in Support (m *' p) & S₁[x,y] ) ; :: thesis: verum

end;

consider f being Function of (Support p),(Support (m *' p)) such that
A5: for x being object st x in Support p holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);

A6: now :: thesis: ( Support (m *' p) = {} implies Support p = {} )

assume A7: Support (m *' p) = {} ; :: thesis: Support p = {}

now :: thesis: not Support p <> {}

assume Support p <> {} ; :: thesis: contradiction
then p <> 0_ (n,L) by POLYNOM7:1;
then reconsider p9 = p as non-zero Polynomial of n,L by POLYNOM7:def 1;
(HT (m, the connected admissible TermOrder of n)) + (HT (p9, the connected admissible TermOrder of n)) in Support (m *' p9) by TERMORD:29;
hence contradiction by A7; :: thesis: verum

end;

hence Support p = {} ; :: thesis: verum

end;

then A8: Support p c= dom f by FUNCT_2:def 1;
A9: Support (m *' p) c= { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support p ) } by TERMORD:30;

A10: now :: thesis: for u being object st u in Support (m *' p) holds
u in f .: (Support p)

let u be object ; :: thesis: ( u in Support (m *' p) implies u in f .: (Support p) )
assume A11: u in Support (m *' p) ; :: thesis: u in f .: (Support p)
then reconsider u9 = u as Element of Bags n ;
u9 in { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support p ) } by A9, A11;
then consider s, t being Element of Bags n such that
A12: ( u9 = s + t & s in Support m ) and
A13: t in Support p ;
A14: t in dom f by A6, A13, FUNCT_2:def 1;
A15: t = In (t,(Bags n)) ;
u9 = (term m) + t by A1, A12, TARSKI:def 1;
then u9 = f . t by A5, A13, A15;
hence u in f .: (Support p) by A14, FUNCT_1:def 6; :: thesis: verum

end;

now :: thesis: for x1, x2 being object st x1 in Support p & x2 in Support p & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in Support p & x2 in Support p & f . x1 = f . x2 implies x1 = x2 )
assume that
A16: x1 in Support p and
A17: x2 in Support p and
A18: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x19 = x1, x29 = x2 as Element of Bags n by A16, A17;
A19: x29 = In (x29,(Bags n)) ;
x19 = In (x19,(Bags n)) ;
then (term m) + x19 = f . x29 by A5, A16, A18
.= (term m) + x29 by A5, A17, A19 ;
hence x1 = (x29 + (term m)) -' (term m) by PRE_POLY:48
.= x2 by PRE_POLY:48 ;
:: thesis: verum

end;

then f is one-to-one by A6, FUNCT_2:19;
then A20: Support p,f .: (Support p) are_equipotent by A8, CARD_1:33;
for u being object st u in f .: (Support p) holds
u in Support (m *' p) ;
then f .: (Support p) = Support (m *' p) by A10, TARSKI:2;
hence card (Support p) = card (Support (m *' p)) by A20, CARD_1:5; :: thesis: verum