:: deftheorem Def12 defines JsqrtSeries POLYNOM9:def 12 :
for L being non empty 1-sorted
for m being set
for P, b₄ being Series of m,L holds
( b₄ = JsqrtSeries P iff for b being bag of m holds b₄ . b = P . ((2 (#) b) +* (0,(b . 0))) );