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

HT (p,T) in Support (Up (p,T,i))

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

HT (p,T) in Support (Up (p,T,i))

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

HT (p,T) in Support (Up (p,T,i))

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

HT (p,T) in Support (Up (p,T,i))

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= card (Support p) implies HT (p,T) in Support (Up (p,T,i)) )

assume that

A1: 1 <= i and

A2: i <= card (Support p) ; :: thesis: HT (p,T) in Support (Up (p,T,i))

Support p <> {} by A1, A2;

then A3: HT (p,T) in Support p by TERMORD:def 6;

set u = Up (p,T,i);

set x = the Element of Support (Up (p,T,i));

A4: Support (Up (p,T,i)) = Upper_Support (p,T,i) by A2, Lm3;

then card (Support (Up (p,T,i))) <> 0 by A1, A2, Def2;

then A5: Support (Up (p,T,i)) <> {} ;

then A6: the Element of Support (Up (p,T,i)) in Support (Up (p,T,i)) ;

then reconsider x = the Element of Support (Up (p,T,i)) as Element of Bags n ;

Support (Up (p,T,i)) c= Support p by A2, A4, Def2;

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

hence HT (p,T) in Support (Up (p,T,i)) by A2, A4, A5, A3, Def2; :: thesis: verum

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

HT (p,T) in Support (Up (p,T,i))

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

HT (p,T) in Support (Up (p,T,i))

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

HT (p,T) in Support (Up (p,T,i))

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

HT (p,T) in Support (Up (p,T,i))

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= card (Support p) implies HT (p,T) in Support (Up (p,T,i)) )

assume that

A1: 1 <= i and

A2: i <= card (Support p) ; :: thesis: HT (p,T) in Support (Up (p,T,i))

Support p <> {} by A1, A2;

then A3: HT (p,T) in Support p by TERMORD:def 6;

set u = Up (p,T,i);

set x = the Element of Support (Up (p,T,i));

A4: Support (Up (p,T,i)) = Upper_Support (p,T,i) by A2, Lm3;

then card (Support (Up (p,T,i))) <> 0 by A1, A2, Def2;

then A5: Support (Up (p,T,i)) <> {} ;

then A6: the Element of Support (Up (p,T,i)) in Support (Up (p,T,i)) ;

then reconsider x = the Element of Support (Up (p,T,i)) as Element of Bags n ;

Support (Up (p,T,i)) c= Support p by A2, A4, Def2;

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

hence HT (p,T) in Support (Up (p,T,i)) by A2, A4, A5, A3, Def2; :: thesis: verum