theorem Th17: :: HILB10_2:17

for n being Nat
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L holds
( len (SgmX ((BagOrder n),(Support p))) = len (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) & ( for i being Nat st 1 <= i & i <= len (SgmX ((BagOrder n),(Support p))) holds
(SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i = ((SgmX ((BagOrder n),(Support p))) /. i) bag_extend 0 ) )