set C = JsqrtSeries P;
deffunc H₁( bag of m) -> set = (2 (#) L) +* (0,(L . 0));
defpred S₁[ bag of m, bag of m] means L = H₁(m);
set S = { x where x is Element of Bags m : ex w being Element of Bags m st
( S₁[w,x] & w in Support P ) } ;
A1: Support P is finite by POLYNOM1:def 5;
A2: for w, x, y being Element of Bags m st S₁[w,x] & S₁[w,y] holds
x = y by Th20;
A3: { x where x is Element of Bags m : ex w being Element of Bags m st
( S₁[w,x] & w in Support P ) } is finite from FRAENKEL:sch 28(A1, A2);
A4: ( dom (JsqrtSeries P) = Bags m & Bags m = dom P ) by FUNCT_2:def 1;
Support (JsqrtSeries P) c= { x where x is Element of Bags m : ex w being Element of Bags m st
( S₁[w,x] & w in Support P ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Support (JsqrtSeries P) or x in { x where x is Element of Bags m : ex w being Element of Bags m st
( S₁[w,x] & w in Support P ) } )
assume A5: x in Support (JsqrtSeries P) ; :: thesis: x in { x where x is Element of Bags m : ex w being Element of Bags m st
( S₁[w,x] & w in Support P ) }
then A6: ( x in dom (JsqrtSeries P) & (JsqrtSeries P) . x <> 0. L ) by POLYNOM1:def 3;
reconsider x = x as bag of m by A5;
A7: H₁(x) in Bags m by PRE_POLY:def 12;
(JsqrtSeries P) . x = P . H₁(x) by Def12;
then H₁(x) in Support P by A7, A6, A4, POLYNOM1:def 3;
hence x in { x where x is Element of Bags m : ex w being Element of Bags m st
( S₁[w,x] & w in Support P ) } by A5; :: thesis: verum

end;

hence JsqrtSeries P is finite-Support by A3, POLYNOM1:def 5; :: thesis: verum