theorem Th24:
for
n being
Ordinal 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
i <= card (Support p) holds
(
Lower_Support (
p,
T,
i)
c= Support p &
card (Lower_Support (p,T,i)) = (card (Support p)) - i & ( for
b,
b9 being
bag of
n st
b in Lower_Support (
p,
T,
i) &
b9 in Support p &
b9 <= b,
T holds
b9 in Lower_Support (
p,
T,
i) ) )