let n be Ordinal; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis:
let p be Polynomial of n,L; :: thesis:
let m be non-zero Monomial of n,L; :: thesis:
let i be Element of NAT ; :: thesis:
set l = Low p,T,i;
assume A1: i <= card (Support p) ; :: thesis:
then A2: Support (Low p,T,i) c= Support p by Th26;
A3: Support (Up p,T,i) = Upper_Support p,T,i by A1, Lm3;
then A4: card (Support (Up p,T,i)) = i by A1, Def2;
A5: Support (Up p,T,i) c= Support p by A1, Th26;
A6: Support (Low p,T,i) = Lower_Support p,T,i by A1, Lm3;
let b be bag of n; :: thesis:
A7: i <= card (Support (m *' p)) by A1, Th10;
then A8: Support (Low (m *' p),T,i) = Lower_Support (m *' p),T,i by Lm3;
A9: Support (Low (m *' p),T,i) c= Support (m *' p) by A7, Th26;
A10: Support (Up (m *' p),T,i) c= Support (m *' p) by A7, Th26;
A11: Support (Up (m *' p),T,i) = Upper_Support (m *' p),T,i by A7, Lm3;
then A12: card (Support (Up (m *' p),T,i)) = i by A7, Def2;
then A13: ( Support (Up p,T,i) = {} implies Support (Up (m *' p),T,i) = {} ) by A4;

A14: now

assume A15: (term m) + b in Support (Low (m *' p),T,i) ; :: thesis:

A16: now

assume (term m) + b in Support (Up (m *' p),T,i) ; :: thesis:
then (term m) + b in (Support (Up (m *' p),T,i)) /\ (Support (Low (m *' p),T,i)) by A15, XBOOLE_0:def 4;
hence contradiction by A7, A9, A15, Th28; :: thesis:

end;

A17: Support (m *' p) = { ((term m) + u) where u is Element of Bags n : u in Support p } by Th9;

A18: now

defpred S₁[ set , set ] means $1 = (term m) + ((In $2,(Bags n)) @ );
assume A19: b in Support (Up p,T,i) ; :: thesis:

A20: now

let b9 be bag of n; :: thesis:
assume A21: (term m) + b9 in Support (Up (m *' p),T,i) ; :: thesis:
then A22: (term m) + b < (term m) + b9,T by A7, A11, A8, A15, Th20;

now

assume b9 <= b,T ; :: thesis:
then (term m) + b9 <= (term m) + b,T by Th2;
hence contradiction by A22, TERMORD:5; :: thesis:

end;

then b < b9,T by TERMORD:5;
then A23: b <= b9,T by TERMORD:def 3;
b9 in Support p by A10, A21, Th8;
hence b9 in Support (Up p,T,i) by A1, A3, A19, A23, Def2; :: thesis:

end;

A24: for x being set st x in Support (Up (m *' p),T,i) holds
ex y being set st
( y in Support (Up p,T,i) & S₁[x,y] )

proof

let x be set ; :: thesis:
assume A25: x in Support (Up (m *' p),T,i) ; :: thesis:
then x in Support (m *' p) by A10;
then consider x9 being Element of Bags n such that
A26: x = (term m) + x9 and
x9 in Support p by A17;
take x9 ; :: thesis:
x9 = In x9,(Bags n) by FUNCT_7:def 1
.= (In x9,(Bags n)) @ by POLYNOM2:def 3 ;
hence ( x9 in Support (Up p,T,i) & S₁[x,x9] ) by A20, A25, A26; :: thesis:

end;

consider f being Function of (Support (Up (m *' p),T,i)),(Support (Up p,T,i)) such that
A27: for x being set st x in Support (Up (m *' p),T,i) holds
S₁[x,f . x] from FUNCT_2:sch 1(A24);

now

let x1, x2 be set ; :: thesis:
assume that
A28: x1 in dom f and
A29: x2 in dom f and
A30: f . x1 = f . x2 ; :: thesis:
f . x2 in rng f by A29, FUNCT_1:12;
then A31: f . x2 in Support (Up p,T,i) ;
f . x1 in rng f by A28, FUNCT_1:12;
then f . x1 in Support (Up p,T,i) ;
then reconsider x19 = f . x1, x29 = f . x2 as Element of Bags n by A31;
A32: x19 = In x19,(Bags n) by FUNCT_7:def 1
.= (In x19,(Bags n)) @ by POLYNOM2:def 3 ;
x29 = In x29,(Bags n) by FUNCT_7:def 1
.= (In x29,(Bags n)) @ by POLYNOM2:def 3 ;
hence x1 = (term m) + x19 by A27, A28, A30
.= x2 by A27, A29, A30, A32 ;
:: thesis:

end;

then A33: f is one-to-one by FUNCT_1:def 8;
Support (Up (m *' p),T,i) c= dom f by A13, FUNCT_2:def 1;
then Support (Up (m *' p),T,i),f .: (Support (Up (m *' p),T,i)) are_equipotent by A33, CARD_1:60;
then card (f .: (Support (Up (m *' p),T,i))) = card (Support (Up (m *' p),T,i)) by CARD_1:21
.= i by A7, A11, Def2 ;
then b in f .: (Support (Up (m *' p),T,i)) by A4, A19, PRE_POLY:8;
then consider bb being set such that
A34: bb in dom f and
A35: ( bb in Support (Up (m *' p),T,i) & f . bb = b ) by FUNCT_1:def 12;
f . bb in rng f by A34, FUNCT_1:12;
then f . bb in Support (Up p,T,i) ;
then reconsider bb9 = f . bb as Element of Bags n ;
bb9 = In bb9,(Bags n) by FUNCT_7:def 1
.= (In bb9,(Bags n)) @ by POLYNOM2:def 3 ;
hence contradiction by A16, A27, A35; :: thesis:

end;

(term m) + b in Support (m *' p) by A9, A15;
then (term m) + b in { ((term m) + u) where u is Element of Bags n : u in Support p } by Th9;
then consider u being Element of Bags n such that
A36: (term m) + b = (term m) + u and
A37: u in Support p ;
b = ((term m) + b) -' (term m) by PRE_POLY:48
.= u by A36, PRE_POLY:48 ;
hence b in Support (Low p,T,i) by A1, A37, A18, Th28; :: thesis:

end;

A38: ( Support (Up (m *' p),T,i) = {} implies Support (Up p,T,i) = {} ) by A12, A4;

now

assume A39: b in Support (Low p,T,i) ; :: thesis:

A40: now

assume b in Support (Up p,T,i) ; :: thesis:
then b in (Support (Up p,T,i)) /\ (Support (Low p,T,i)) by A39, XBOOLE_0:def 4;
hence contradiction by A1, A2, A39, Th28; :: thesis:

end;

A41: now

defpred S₁[ set , set ] means $2 = (term m) + ((In $1,(Bags n)) @ );
assume A42: (term m) + b in Support (Up (m *' p),T,i) ; :: thesis:

A43: now

let b9 be bag of n; :: thesis:
assume A44: b9 in Support (Up p,T,i) ; :: thesis:
then (term m) + b < (term m) + b9,T by A1, A3, A6, A39, Th4, Th20;
then A45: (term m) + b <= (term m) + b9,T by TERMORD:def 3;
(term m) + b9 in Support (m *' p) by A5, A44, Th8;
hence (term m) + b9 in Support (Up (m *' p),T,i) by A7, A11, A42, A45, Def2; :: thesis:

end;

A46: for x being set st x in Support (Up p,T,i) holds
ex y being set st
( y in Support (Up (m *' p),T,i) & S₁[x,y] )

proof

let x be set ; :: thesis:
assume A47: x in Support (Up p,T,i) ; :: thesis:
then reconsider x9 = x as Element of Bags n ;
take (term m) + x9 ; :: thesis:
x9 = In x9,(Bags n) by FUNCT_7:def 1
.= (In x9,(Bags n)) @ by POLYNOM2:def 3 ;
hence ( (term m) + x9 in Support (Up (m *' p),T,i) & S₁[x,(term m) + x9] ) by A43, A47; :: thesis:

end;

consider f being Function of (Support (Up p,T,i)),(Support (Up (m *' p),T,i)) such that
A48: for x being set st x in Support (Up p,T,i) holds
S₁[x,f . x] from FUNCT_2:sch 1(A46);

now

let x1, x2 be set ; :: thesis:
assume that
A49: x1 in dom f and
A50: x2 in dom f and
A51: f . x1 = f . x2 ; :: thesis:
( x1 in Support (Up p,T,i) & x2 in Support (Up p,T,i) ) by A49, A50;
then reconsider x = x1, y = x2 as Element of Bags n ;
y = In y,(Bags n) by FUNCT_7:def 1
.= (In y,(Bags n)) @ by POLYNOM2:def 3 ;
then A52: f . y = (term m) + y by A48, A50;
x = In x,(Bags n) by FUNCT_7:def 1
.= (In x,(Bags n)) @ by POLYNOM2:def 3 ;
then A53: f . x = (term m) + x by A48, A49;
thus x1 = ((term m) + x) -' (term m) by PRE_POLY:48
.= x2 by A51, A53, A52, PRE_POLY:48 ; :: thesis:

end;

then A54: f is one-to-one by FUNCT_1:def 8;
Support (Up p,T,i) c= dom f by A38, FUNCT_2:def 1;
then Support (Up p,T,i),f .: (Support (Up p,T,i)) are_equipotent by A54, CARD_1:60;
then card (f .: (Support (Up p,T,i))) = card (Support (Up p,T,i)) by CARD_1:21
.= i by A1, A3, Def2 ;
then (term m) + b in f .: (Support (Up p,T,i)) by A12, A42, PRE_POLY:8;
then consider bb being set such that
A55: bb in dom f and
A56: bb in Support (Up p,T,i) and
A57: f . bb = (term m) + b by FUNCT_1:def 12;
reconsider bb = bb as Element of Bags n by A56;
bb = In bb,(Bags n) by FUNCT_7:def 1
.= (In bb,(Bags n)) @ by POLYNOM2:def 3 ;
then A58: (term m) + bb = (term m) + b by A48, A55, A57;
bb = ((term m) + bb) -' (term m) by PRE_POLY:48
.= b by A58, PRE_POLY:48 ;
hence contradiction by A40, A55; :: thesis:

end;

(term m) + b in Support (m *' p) by A2, A39, Th8;
hence (term m) + b in Support (Low (m *' p),T,i) by A7, A41, Th28; :: thesis:

end;

hence ( (term m) + b in Support (Low (m *' p),T,i) iff b in Support (Low p,T,i) ) by A14; :: thesis: