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))
A1: 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;
m <> 0_ n,L by POLYNOM7:def 2;
then Support m <> {} by POLYNOM7:1;
then A2: Support m = {(term m)} by POLYNOM7:7;
defpred S₁[ set , set ] means $2 = (term m) + ((In $1,(Bags n)) @ );
A3: for x being set st x in Support p holds
ex y being set st
( y in Support (m *' p) & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in Support p implies ex y being set st
( y in Support (m *' p) & S₁[x,y] ) )
assume A4: x in Support p ; :: thesis: ex y being set st
( y in Support (m *' p) & S₁[x,y] )
then reconsider x' = x as Element of Bags n ;
A5: x' = In x',(Bags n) by FUNCT_7:def 1
.= (In x',(Bags n)) @ by POLYNOM2:def 3 ;
(term m) + x' in Support (m *' p) by A4, Th8;
hence ex y being set st
( y in Support (m *' p) & S₁[x,y] ) by A5; :: thesis: verum

end;

consider T being connected admissible TermOrder of n;
consider f being Function of (Support p),(Support (m *' p)) such that
A6: for x being set st x in Support p holds
S₁[x,f . x] from FUNCT_2:sch 1(A3);

A7: now

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

now

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

end;

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

end;

then A9: Support p c= dom f by FUNCT_2:def 1;

now

let x1, x2 be set ; :: thesis: ( x1 in Support p & x2 in Support p & f . x1 = f . x2 implies x1 = x2 )
assume A10: ( x1 in Support p & x2 in Support p & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then reconsider x1' = x1, x2' = x2 as Element of Bags n ;
A11: x2' = In x2',(Bags n) by FUNCT_7:def 1
.= (In x2',(Bags n)) @ by POLYNOM2:def 3 ;
x1' = In x1',(Bags n) by FUNCT_7:def 1
.= (In x1',(Bags n)) @ by POLYNOM2:def 3 ;
then (term m) + x1' = f . x2' by A6, A10
.= (term m) + x2' by A6, A10, A11 ;
hence x1 = (x2' + (term m)) -' (term m) by POLYNOM1:52
.= x2 by POLYNOM1:52 ;
:: thesis: verum

end;

then f is one-to-one by A7, FUNCT_2:25;
then A12: Support p,f .: (Support p) are_equipotent by A9, CARD_1:60;
A13: for u being set st u in f .: (Support p) holds
u in Support (m *' p) ;

now

let u be set ; :: thesis: ( u in Support (m *' p) implies u in f .: (Support p) )
assume A14: u in Support (m *' p) ; :: thesis: u in f .: (Support p)
then reconsider u' = u as Element of Bags n ;
u' in { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support p ) } by A1, A14;
then consider s, t being Element of Bags n such that
A15: ( u' = s + t & s in Support m & t in Support p ) ;
A16: t = In t,(Bags n) by FUNCT_7:def 1
.= (In t,(Bags n)) @ by POLYNOM2:def 3 ;
u' = (term m) + t by A2, A15, TARSKI:def 1;
then A17: u' = f . t by A6, A15, A16;
t in dom f by A7, A15, FUNCT_2:def 1;
hence u in f .: (Support p) by A17, FUNCT_1:def 12; :: thesis: verum

end;

then f .: (Support p) = Support (m *' p) by A13, TARSKI:2;
hence card (Support p) = card (Support (m *' p)) by A12, CARD_1:21; :: thesis: verum