set c = JsqrtSeries M;
A2: ( dom (JsqrtSeries M) = Bags m & Bags m = dom M ) by FUNCT_2:def 1;
A3: rng (JsqrtSeries M) c= INT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (JsqrtSeries M) or y in INT )
assume A4: y in rng (JsqrtSeries M) ; :: thesis: y in INT
consider x being object such that
A5: ( x in dom (JsqrtSeries M) & (JsqrtSeries M) . x = y ) by A4, FUNCT_1:def 3;
reconsider x = x as bag of m by A5;

per cases ( not x in Support (JsqrtSeries M) or x in Support (JsqrtSeries M) ) ;

suppose not x in Support (JsqrtSeries M) ; :: thesis: y in INT

then (JsqrtSeries M) . x = 0. F_Complex by A5, POLYNOM1:def 3
.= 0 by COMPLFLD:def 1 ;
hence y in INT by A5, INT_1:def 2; :: thesis: verum

end;

suppose x in Support (JsqrtSeries M) ; :: thesis: y in INT

then A6: (JsqrtSeries M) . x <> 0. F_Complex by POLYNOM1:def 4;
A7: (2 (#) x) +* (0,(x . 0)) in Bags m by PRE_POLY:def 12;
A8: (JsqrtSeries M) . x = M . ((2 (#) x) +* (0,(x . 0))) by Def12;
then (2 (#) x) +* (0,(x . 0)) in Support M by A7, A2, A6, POLYNOM1:def 3;
then consider i being Integer such that
A9: M . ((2 (#) x) +* (0,(x . 0))) = i '*' (1_ F_Complex) by A1, Def10;
M . ((2 (#) x) +* (0,(x . 0))) = i by A9, Th1;
hence y in INT by A5, A8, INT_1:def 2; :: thesis: verum

end;

end;

end;

then rng (JsqrtSeries M) c= REAL by NUMBERS:15;
then reconsider r = JsqrtSeries M as Series of m,F_Real by A2, FUNCT_2:2;
A10: 0. F_Complex = 0. F_Real by COMPLFLD:def 1;
A11: Support r c= Support (JsqrtSeries M)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Support r or y in Support (JsqrtSeries M) )
assume y in Support r ; :: thesis: y in Support (JsqrtSeries M)
then ( y in dom r & r . y <> 0. F_Real ) by POLYNOM1:def 3;
hence y in Support (JsqrtSeries M) by A10, POLYNOM1:def 3; :: thesis: verum

end;

reconsider r = r as Polynomial of m,F_Real by A11, POLYNOM1:def 5;
rng r c= INT by A3;
hence JsqrtSeries M is INT -valued Polynomial of m,F_Real by RELAT_1:def 19; :: thesis: verum