let n be Ordinal; :: thesis: for T being connected TermOrder of n

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st 0 < i & i < card (Support p) holds

HT ((Low (p,T,i)),T) < HT (p,T),T

let T be connected TermOrder of n; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st 0 < i & i < card (Support p) holds

HT ((Low (p,T,i)),T) < HT (p,T),T

let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L

for i being Element of NAT st 0 < i & i < card (Support p) holds

HT ((Low (p,T,i)),T) < HT (p,T),T

let p be Polynomial of n,L; :: thesis: for i being Element of NAT st 0 < i & i < card (Support p) holds

HT ((Low (p,T,i)),T) < HT (p,T),T

let i be Element of NAT ; :: thesis: ( 0 < i & i < card (Support p) implies HT ((Low (p,T,i)),T) < HT (p,T),T )

assume that

A1: 0 < i and

A2: i < card (Support p) ; :: thesis: HT ((Low (p,T,i)),T) < HT (p,T),T

set l = Low (p,T,i);

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st 0 < i & i < card (Support p) holds

HT ((Low (p,T,i)),T) < HT (p,T),T

let T be connected TermOrder of n; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for i being Element of NAT st 0 < i & i < card (Support p) holds

HT ((Low (p,T,i)),T) < HT (p,T),T

let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L

for i being Element of NAT st 0 < i & i < card (Support p) holds

HT ((Low (p,T,i)),T) < HT (p,T),T

let p be Polynomial of n,L; :: thesis: for i being Element of NAT st 0 < i & i < card (Support p) holds

HT ((Low (p,T,i)),T) < HT (p,T),T

let i be Element of NAT ; :: thesis: ( 0 < i & i < card (Support p) implies HT ((Low (p,T,i)),T) < HT (p,T),T )

assume that

A1: 0 < i and

A2: i < card (Support p) ; :: thesis: HT ((Low (p,T,i)),T) < HT (p,T),T

set l = Low (p,T,i);

now :: thesis: ( ( Low (p,T,i) = 0_ (n,L) & contradiction ) or ( Low (p,T,i) <> 0_ (n,L) & HT ((Low (p,T,i)),T) < HT (p,T),T ) )end;

hence
HT ((Low (p,T,i)),T) < HT (p,T),T
; :: thesis: verumper cases
( Low (p,T,i) = 0_ (n,L) or Low (p,T,i) <> 0_ (n,L) )
;

end;

case
Low (p,T,i) = 0_ (n,L)
; :: thesis: contradiction

then A3:
card (Support (Low (p,T,i))) = 0
by CARD_1:27, POLYNOM7:1;

Support (Low (p,T,i)) = Lower_Support (p,T,i) by A2, Lm3;

then 0 + i = ((card (Support p)) - i) + i by A2, A3, Th24;

hence contradiction by A2; :: thesis: verum

end;Support (Low (p,T,i)) = Lower_Support (p,T,i) by A2, Lm3;

then 0 + i = ((card (Support p)) - i) + i by A2, A3, Th24;

hence contradiction by A2; :: thesis: verum

case A4:
Low (p,T,i) <> 0_ (n,L)
; :: thesis: HT ((Low (p,T,i)),T) < HT (p,T),T

A5:
Support (Low (p,T,i)) c= Support p
by A2, Th26;

A6: Support (Low (p,T,i)) = Lower_Support (p,T,i) by A2, Lm3;

then A11: HT ((Low (p,T,i)),T) in Support (Low (p,T,i)) by TERMORD:def 6;

then HT ((Low (p,T,i)),T) <= HT (p,T),T by A5, TERMORD:def 6;

hence HT ((Low (p,T,i)),T) < HT (p,T),T by A7, A11, TERMORD:def 3; :: thesis: verum

end;A6: Support (Low (p,T,i)) = Lower_Support (p,T,i) by A2, Lm3;

A7: now :: thesis: not HT (p,T) in Support (Low (p,T,i))

Support (Low (p,T,i)) <> {}
by A4, POLYNOM7:1;assume A8:
HT (p,T) in Support (Low (p,T,i))
; :: thesis: contradiction

u in Support p by A5;

then card (Support p) = card (Support (Low (p,T,i))) by A9, TARSKI:2

.= (card (Support p)) - i by A2, A6, Th24 ;

hence contradiction by A1; :: thesis: verum

end;A9: now :: thesis: for u being object st u in Support p holds

u in Support (Low (p,T,i))

for u being object st u in Support (Low (p,T,i)) holds u in Support (Low (p,T,i))

let u be object ; :: thesis: ( u in Support p implies u in Support (Low (p,T,i)) )

assume A10: u in Support p ; :: thesis: u in Support (Low (p,T,i))

then reconsider x = u as Element of Bags n ;

x <= HT (p,T),T by A10, TERMORD:def 6;

hence u in Support (Low (p,T,i)) by A2, A6, A8, A10, Th24; :: thesis: verum

end;assume A10: u in Support p ; :: thesis: u in Support (Low (p,T,i))

then reconsider x = u as Element of Bags n ;

x <= HT (p,T),T by A10, TERMORD:def 6;

hence u in Support (Low (p,T,i)) by A2, A6, A8, A10, Th24; :: thesis: verum

u in Support p by A5;

then card (Support p) = card (Support (Low (p,T,i))) by A9, TARSKI:2

.= (card (Support p)) - i by A2, A6, Th24 ;

hence contradiction by A1; :: thesis: verum

then A11: HT ((Low (p,T,i)),T) in Support (Low (p,T,i)) by TERMORD:def 6;

then HT ((Low (p,T,i)),T) <= HT (p,T),T by A5, TERMORD:def 6;

hence HT ((Low (p,T,i)),T) < HT (p,T),T by A7, A11, TERMORD:def 3; :: thesis: verum