let L be non empty ZeroStr ; :: thesis: 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)) ) )
let m be Nat; :: thesis: 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)) ) )
let p be Polynomial of m,L; :: thesis: ( ( for b being bag of m
for n being Nat st b in Support p holds
b . n is even ) implies 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)) ) ) )
assume A1: for b being bag of m
for n being Nat st b in Support p holds
b . n is even ; :: thesis: 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)) ) )
let CS be one-to-one FinSequence of Bags m; :: thesis: ( rng CS = Support (JsqrtSeries p) implies 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)) ) ) )
assume A2: rng CS = Support (JsqrtSeries p) ; :: thesis: 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)) ) )
deffunc H1( bag of m) -> set = (2 (#) $1) +* (0,($1 . 0));
deffunc H2( object ) -> set = H1(CS /. $1);
consider S being FinSequence such that
A3: ( len S = len CS & ( for k being Nat st k in dom S holds
S . k = H2(k) ) ) from FINSEQ_1:sch 2();
 A4: dom S = dom CS by A3, FINSEQ_3:29;
A5: rng S c= Support p
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng S or y in Support p )
assume A6: y in rng S ; :: thesis: y in Support p
consider x being object such that
A7: ( x in dom S & S . x = y ) by A6, FUNCT_1:def 3;
reconsider x = x as Nat by A7;
A8: (JsqrtSeries p) . (CS /. x) = p . H1(CS /. x) by Def12;
A9: H1(CS /. x) in Bags m by PRE_POLY:def 12;
( CS . x = CS /. x & CS . x in rng CS ) by A7, A4, FUNCT_1:def 3, PARTFUN1:def 6;
then (JsqrtSeries p) . (CS /. x) <> 0. L by A2, POLYNOM1:def 4;
then H1(CS /. x) in Support p by A8, A9, POLYNOM1:def 4;
hence y in Support p by A7, A3; :: thesis: verum
end;
A10: Support p c= rng S
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Support p or b in rng S )
assume A11: b in Support p ; :: thesis: b in rng S
A12: ( b in dom p & p . b <> 0. L ) by A11, POLYNOM1:def 3;
reconsider b = b as bag of m by A11;
defpred S1[ object , object ] means ( ( $1 = 0 implies $2 = b . 0 ) & ( $1 <> 0 implies $2 = (1 / 2) * (b . $1) ) );
A13: for x being object st x in m holds
ex y being object st
( y in NAT & S1[x,y] )
proof
let x be object ; :: thesis: ( x in m implies ex y being object st
( y in NAT & S1[x,y] ) )
assume A14: x in m ; :: thesis: ex y being object st
( y in NAT & S1[x,y] )
x in Segm m by A14;
then reconsider x = x as Nat ;
b . x is even by A11, A1;
then consider i being Nat such that
A15: b . x = 2 * i by ABIAN:def 2;
per cases ( x = 0 or x <> 0 ) ;
suppose A16: x = 0 ; :: thesis: ex y being object st
( y in NAT & S1[x,y] )
take b . x ; :: thesis: ( b . x in NAT & S1[x,b . x] )
thus ( b . x in NAT & S1[x,b . x] ) by A16, ORDINAL1:def 12; :: thesis: verum
end;
suppose A17: x <> 0 ; :: thesis: ex y being object st
( y in NAT & S1[x,y] )
take i ; :: thesis: ( i in NAT & S1[x,i] )
thus ( i in NAT & S1[x,i] ) by A17, A15, ORDINAL1:def 12; :: thesis: verum
end;
end;
end;
consider f being Function such that
A18: ( dom f = m & rng f c= NAT & ( for x being object st x in m holds
S1[x,f . x] ) ) from FUNCT_1:sch 6(A13);
 reconsider f = f as ManySortedSet of m by A18, RELAT_1:def 18, PARTFUN1:def 2;
reconsider f = f as bag of m by A18, VALUED_0:def 6;
A19: f in Bags m by PRE_POLY:def 12;
A20: ( dom b = m & m = dom (2 (#) f) & m = dom ((2 (#) f) +* (0,(f . 0))) ) by PARTFUN1:def 2;
for x being object st x in m holds
b . x = ((2 (#) f) +* (0,(f . 0))) . x
proof
let x be object ; :: thesis: ( x in m implies b . x = ((2 (#) f) +* (0,(f . 0))) . x )
assume A21: x in m ; :: thesis: b . x = ((2 (#) f) +* (0,(f . 0))) . x
per cases ( x = 0 or x <> 0 ) ;
suppose A22: x = 0 ; :: thesis: b . x = ((2 (#) f) +* (0,(f . 0))) . x
hence ((2 (#) f) +* (0,(f . 0))) . x = f . 0 by A21, A20, FUNCT_7:31
.= b . x by A22, A18, A21 ;
:: thesis: verum
end;
suppose A23: x <> 0 ; :: thesis: b . x = ((2 (#) f) +* (0,(f . 0))) . x
hence ((2 (#) f) +* (0,(f . 0))) . x = (2 (#) f) . x by FUNCT_7:32
.= 2 * (f . x) by VALUED_1:6
.= 2 * ((1 / 2) * (b . x)) by A23, A18, A21
.= b . x ;
:: thesis: verum
end;
end;
end;
then A24: b = (2 (#) f) +* (0,(f . 0)) by A20;
then (JsqrtSeries p) . f = p . b by Def12;
then f in Support (JsqrtSeries p) by A12, A19, POLYNOM1:def 4;
then consider x being object such that
A25: ( x in dom CS & CS . x = f ) by A2, FUNCT_1:def 3;
reconsider x = x as Nat by A25;
A26: f = CS /. x by A25, PARTFUN1:def 6;
S . x = b by A24, A26, A25, A4, A3;
hence b in rng S by A25, A4, FUNCT_1:def 3; :: thesis: verum
end;
then A27: Support p = rng S by A5, XBOOLE_0:def 10;
S is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom S or not x2 in dom S or not S . x1 = S . x2 or x1 = x2 )
assume A28: ( x1 in dom S & x2 in dom S & S . x1 = S . x2 ) ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Nat by A28;
( H1(CS /. x1) = S . x1 & S . x1 = H1(CS /. x2) ) by A3, A28;
then ( CS . x1 = CS /. x1 & CS /. x1 = CS /. x2 & CS /. x2 = CS . x2 ) by Th20, A4, A28, PARTFUN1:def 6;
hence x1 = x2 by A4, A28, FUNCT_1:def 4; :: thesis: verum
end;
then reconsider S = S as one-to-one FinSequence of Bags m by A27, FINSEQ_1:def 4;
take S ; :: thesis: ( 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)) ) )
thus ( 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)) ) ) by A10, A3, A5, XBOOLE_0:def 10; :: thesis: verum