theorem Th65: :: POLYNOM9:65

for L being non empty ZeroStr
for m being Nat
for p being Polynomial of m,L st ( for b being bag of m
for n being Nat st b in Support p holds
b . n is even ) holds
for CS being one-to-one FinSequence of Bags m st rng CS = Support (JsqrtSeries p) holds
ex S being one-to-one FinSequence of Bags m st
( len S = len CS & rng S = Support p & ( for i being Nat st i in dom S holds
S . i = (2 (#) (CS /. i)) +* (0,((CS /. i) . 0)) ) )