let n be Ordinal; :: thesis: for T being connected admissible 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 i < card (Support p) holds

(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}

let T be connected admissible 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 i < card (Support p) holds

(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),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 i < card (Support p) holds

(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}

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

(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}

let i be Element of NAT ; :: thesis: ( i < card (Support p) implies (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))} )

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

set l1 = Low (p,T,(i + 1));

assume A1: i < card (Support p) ; :: thesis: (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}

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

then A3: card (Support (Low (p,T,i))) = (card (Support p)) - i by A1, Th24;

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

A6: i + 1 <= card (Support p) by A1, NAT_1:13;

then Support (Low (p,T,(i + 1))) = Lower_Support (p,T,(i + 1)) by Lm3;

then A7: card (Support (Low (p,T,(i + 1)))) = (card (Support p)) - (i + 1) by A6, Th24;

then card ((Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1))))) = ((card (Support p)) - i) - ((card (Support p)) - (i + 1)) by A1, A3, Th41, CARD_2:44

.= 1 ;

then consider x being object such that

A8: (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {x} by CARD_2:42;

A9: Support (Low (p,T,(i + 1))) = Lower_Support (p,T,(i + 1)) by A6, Lm3;

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 i < card (Support p) holds

(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}

let T be connected admissible 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 i < card (Support p) holds

(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),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 i < card (Support p) holds

(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}

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

(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}

let i be Element of NAT ; :: thesis: ( i < card (Support p) implies (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))} )

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

set l1 = Low (p,T,(i + 1));

assume A1: i < card (Support p) ; :: thesis: (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}

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

then A3: card (Support (Low (p,T,i))) = (card (Support p)) - i by A1, Th24;

now :: thesis: not Lower_Support (p,T,i) = {}

then A4:
HT ((Low (p,T,i)),T) in Support (Low (p,T,i))
by A2, TERMORD:def 6;assume
Lower_Support (p,T,i) = {}
; :: thesis: contradiction

then (card (Support p)) - i = 0 by A1, Th24, CARD_1:27;

hence contradiction by A1; :: thesis: verum

end;then (card (Support p)) - i = 0 by A1, Th24, CARD_1:27;

hence contradiction by A1; :: thesis: verum

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

A6: i + 1 <= card (Support p) by A1, NAT_1:13;

then Support (Low (p,T,(i + 1))) = Lower_Support (p,T,(i + 1)) by Lm3;

then A7: card (Support (Low (p,T,(i + 1)))) = (card (Support p)) - (i + 1) by A6, Th24;

then card ((Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1))))) = ((card (Support p)) - i) - ((card (Support p)) - (i + 1)) by A1, A3, Th41, CARD_2:44

.= 1 ;

then consider x being object such that

A8: (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {x} by CARD_2:42;

A9: Support (Low (p,T,(i + 1))) = Lower_Support (p,T,(i + 1)) by A6, Lm3;

now :: thesis: not x <> HT ((Low (p,T,i)),T)

hence
(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}
by A8; :: thesis: verumassume A10:
x <> HT ((Low (p,T,i)),T)
; :: thesis: contradiction

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

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

then (card (Support p)) + (- i) <= (card (Support p)) + (- (i + 1)) by A3, A7, A12, TARSKI:2;

then - i <= - (i + 1) by XREAL_1:6;

then i + 1 <= i by XREAL_1:24;

then (i + 1) - i <= i - i by XREAL_1:9;

then 1 <= 0 ;

hence contradiction ; :: thesis: verum

end;A11: now :: thesis: HT ((Low (p,T,i)),T) in Support (Low (p,T,(i + 1)))

assume
not HT ((Low (p,T,i)),T) in Support (Low (p,T,(i + 1)))
; :: thesis: contradiction

then HT ((Low (p,T,i)),T) in (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) by A4, XBOOLE_0:def 5;

hence contradiction by A8, A10, TARSKI:def 1; :: thesis: verum

end;then HT ((Low (p,T,i)),T) in (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) by A4, XBOOLE_0:def 5;

hence contradiction by A8, A10, TARSKI:def 1; :: thesis: verum

A12: now :: thesis: for u being object st u in Support (Low (p,T,i)) holds

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

Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i))
by A1, Th41;u in Support (Low (p,T,(i + 1)))

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

assume A13: u in Support (Low (p,T,i)) ; :: thesis: u in Support (Low (p,T,(i + 1)))

then reconsider u9 = u as Element of Bags n ;

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

hence u in Support (Low (p,T,(i + 1))) by A6, A5, A9, A11, A13, Th24; :: thesis: verum

end;assume A13: u in Support (Low (p,T,i)) ; :: thesis: u in Support (Low (p,T,(i + 1)))

then reconsider u9 = u as Element of Bags n ;

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

hence u in Support (Low (p,T,(i + 1))) by A6, A5, A9, A11, A13, Th24; :: thesis: verum

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

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

then (card (Support p)) + (- i) <= (card (Support p)) + (- (i + 1)) by A3, A7, A12, TARSKI:2;

then - i <= - (i + 1) by XREAL_1:6;

then i + 1 <= i by XREAL_1:24;

then (i + 1) - i <= i - i by XREAL_1:9;

then 1 <= 0 ;

hence contradiction ; :: thesis: verum