let n, m be Nat; :: thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of (n + m),L st vars p c= n holds
ex q being Polynomial of n,L st
( vars q c= n & rng q c= rng p & ( for b being bag of n + m holds
( ( b | n in Support q & ( for i being Nat st i >= n holds
b . i = 0 ) ) iff b in Support p ) ) & ( for b being bag of n + m st b in Support p holds
q . (b | n) = p . b ) & ( for x being Function of (n + m),L
for y being Function of n,L st x | n = y holds
eval (p,x) = eval (q,y) ) )
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of (n + m),L st vars p c= n holds
ex q being Polynomial of n,L st
( vars q c= n & rng q c= rng p & ( for b being bag of n + m holds
( ( b | n in Support q & ( for i being Nat st i >= n holds
b . i = 0 ) ) iff b in Support p ) ) & ( for b being bag of n + m st b in Support p holds
q . (b | n) = p . b ) & ( for x being Function of (n + m),L
for y being Function of n,L st x | n = y holds
eval (p,x) = eval (q,y) ) )
let p be Polynomial of (n + m),L; :: thesis: ( vars p c= n implies ex q being Polynomial of n,L st
( vars q c= n & rng q c= rng p & ( for b being bag of n + m holds
( ( b | n in Support q & ( for i being Nat st i >= n holds
b . i = 0 ) ) iff b in Support p ) ) & ( for b being bag of n + m st b in Support p holds
q . (b | n) = p . b ) & ( for x being Function of (n + m),L
for y being Function of n,L st x | n = y holds
eval (p,x) = eval (q,y) ) ) )
assume A1: vars p c= n ; :: thesis: ex q being Polynomial of n,L st
( vars q c= n & rng q c= rng p & ( for b being bag of n + m holds
( ( b | n in Support q & ( for i being Nat st i >= n holds
b . i = 0 ) ) iff b in Support p ) ) & ( for b being bag of n + m st b in Support p holds
q . (b | n) = p . b ) & ( for x being Function of (n + m),L
for y being Function of n,L st x | n = y holds
eval (p,x) = eval (q,y) ) )
defpred S₁[ Nat] means ( $1 <= m & ex q being Polynomial of (n + $1),L st
( vars q c= n & rng q c= rng p & ( for b being bag of n + m holds
( ( b | (n + $1) in Support q & ( for i being Nat st i >= n + $1 holds
b . i = 0 ) ) iff b in Support p ) ) & ( for b being bag of n + m st b in Support p holds
q . (b | (n + $1)) = p . b ) & ( for x being Function of (n + m),L
for y being Function of (n + $1),L st x | (n + $1) = y holds
eval (p,x) = eval (q,y) ) ) );
A2: ex k being Nat st S₁[k]

proof

take m ; :: thesis: S₁[m]
thus m <= m ; :: thesis: ex q being Polynomial of (n + m),L st
( vars q c= n & rng q c= rng p & ( for b being bag of n + m holds
( ( b | (n + m) in Support q & ( for i being Nat st i >= n + m holds
b . i = 0 ) ) iff b in Support p ) ) & ( for b being bag of n + m st b in Support p holds
q . (b | (n + m)) = p . b ) & ( for x, y being Function of (n + m),L st x | (n + m) = y holds
eval (p,x) = eval (q,y) ) )
take q = p; :: thesis: ( vars q c= n & rng q c= rng p & ( for b being bag of n + m holds
( ( b | (n + m) in Support q & ( for i being Nat st i >= n + m holds
b . i = 0 ) ) iff b in Support p ) ) & ( for b being bag of n + m st b in Support p holds
q . (b | (n + m)) = p . b ) & ( for x, y being Function of (n + m),L st x | (n + m) = y holds
eval (p,x) = eval (q,y) ) )
thus ( vars q c= n & rng q c= rng p ) by A1; :: thesis: ( ( for b being bag of n + m holds
( ( b | (n + m) in Support q & ( for i being Nat st i >= n + m holds
b . i = 0 ) ) iff b in Support p ) ) & ( for b being bag of n + m st b in Support p holds
q . (b | (n + m)) = p . b ) & ( for x, y being Function of (n + m),L st x | (n + m) = y holds
eval (p,x) = eval (q,y) ) )
thus for b being bag of n + m holds
( ( b | (n + m) in Support q & ( for i being Nat st i >= n + m holds
b . i = 0 ) ) iff b in Support p ) :: thesis: ( ( for b being bag of n + m st b in Support p holds
q . (b | (n + m)) = p . b ) & ( for x, y being Function of (n + m),L st x | (n + m) = y holds
eval (p,x) = eval (q,y) ) )

proof

let b be bag of n + m; :: thesis: ( ( b | (n + m) in Support q & ( for i being Nat st i >= n + m holds
b . i = 0 ) ) iff b in Support p )
for i being Nat st i >= n + m holds
b . i = 0

proof

let i be Nat; :: thesis: ( i >= n + m implies b . i = 0 )
assume i >= n + m ; :: thesis: b . i = 0
then not i in Segm (n + m) by NAT_1:44;
then not i in dom b ;
hence b . i = 0 by FUNCT_1:def 2; :: thesis: verum

end;

hence ( ( b | (n + m) in Support q & ( for i being Nat st i >= n + m holds
b . i = 0 ) ) iff b in Support p ) ; :: thesis: verum

end;

thus ( ( for b being bag of n + m st b in Support p holds
q . (b | (n + m)) = p . b ) & ( for x, y being Function of (n + m),L st x | (n + m) = y holds
eval (p,x) = eval (q,y) ) ) ; :: thesis: verum

end;

A3: for k being Nat st k <> 0 & S₁[k] holds
ex n being Nat st
( n < k & S₁[n] )

proof

let k1 be Nat; :: thesis: ( k1 <> 0 & S₁[k1] implies ex n being Nat st
( n < k1 & S₁[n] ) )
assume A4: ( k1 <> 0 & S₁[k1] ) ; :: thesis: ex n being Nat st
( n < k1 & S₁[n] )
consider q being Polynomial of (n + k1),L such that
A5: vars q c= n and
A6: rng q c= rng p and
A7: for b being bag of n + m holds
( ( b | (n + k1) in Support q & ( for i being Nat st i >= n + k1 holds
b . i = 0 ) ) iff b in Support p ) and
A8: for b being bag of n + m st b in Support p holds
q . (b | (n + k1)) = p . b and
A9: for x being Function of (n + m),L
for y being Function of (n + k1),L st x | (n + k1) = y holds
eval (p,x) = eval (q,y) by A4;
reconsider k = k1 - 1 as Nat by A4;
reconsider q1 = q as Polynomial of ((n + k) + 1),L ;
take k ; :: thesis: ( k < k1 & S₁[k] )
k1 = k + 1 ;
hence k < k1 by NAT_1:13; :: thesis: S₁[k]
A10: n + (k + 1) <= n + m by A4, XREAL_1:7;
A11: Segm ((n + k) + 1) c= Segm (n + m) by A4, XREAL_1:7, NAT_1:39;
A12: k + 1 <= m by A4;
thus k <= m by A12, NAT_1:13; :: thesis: ex q being Polynomial of (n + k),L st
( vars q c= n & rng q c= rng p & ( for b being bag of n + m holds
( ( b | (n + k) in Support q & ( for i being Nat st i >= n + k holds
b . i = 0 ) ) iff b in Support p ) ) & ( for b being bag of n + m st b in Support p holds
q . (b | (n + k)) = p . b ) & ( for x being Function of (n + m),L
for y being Function of (n + k),L st x | (n + k) = y holds
eval (p,x) = eval (q,y) ) )
take Q = q1 removed_last ; :: thesis: ( vars Q c= n & rng Q c= rng p & ( for b being bag of n + m holds
( ( b | (n + k) in Support Q & ( for i being Nat st i >= n + k holds
b . i = 0 ) ) iff b in Support p ) ) & ( for b being bag of n + m st b in Support p holds
Q . (b | (n + k)) = p . b ) & ( for x being Function of (n + m),L
for y being Function of (n + k),L st x | (n + k) = y holds
eval (p,x) = eval (Q,y) ) )
A13: vars Q c= (vars q1) \ {(n + k)} by Th52;
( (vars q1) \ {(n + k)} c= n \ {(n + k)} & n \ {(n + k)} c= n ) by A5, XBOOLE_1:35;
hence vars Q c= n by A13; :: thesis: ( rng Q c= rng p & ( for b being bag of n + m holds
( ( b | (n + k) in Support Q & ( for i being Nat st i >= n + k holds
b . i = 0 ) ) iff b in Support p ) ) & ( for b being bag of n + m st b in Support p holds
Q . (b | (n + k)) = p . b ) & ( for x being Function of (n + m),L
for y being Function of (n + k),L st x | (n + k) = y holds
eval (p,x) = eval (Q,y) ) )
A14: ( dom Q = Bags (n + k) & dom q1 = Bags ((n + k) + 1) ) by PARTFUN1:def 2;
thus rng Q c= rng p :: thesis: ( ( for b being bag of n + m holds
( ( b | (n + k) in Support Q & ( for i being Nat st i >= n + k holds
b . i = 0 ) ) iff b in Support p ) ) & ( for b being bag of n + m st b in Support p holds
Q . (b | (n + k)) = p . b ) & ( for x being Function of (n + m),L
for y being Function of (n + k),L st x | (n + k) = y holds
eval (p,x) = eval (Q,y) ) )

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng Q or y in rng p )
assume y in rng Q ; :: thesis: y in rng p
then consider x being object such that
A15: ( x in dom Q & Q . x = y ) by FUNCT_1:def 3;
reconsider x = x as Element of Bags (n + k) by A15;
A16: Q . x = q1 . (x bag_extend 0) by Def6;
q1 . (x bag_extend 0) in rng q1 by A14, FUNCT_1:def 3;
hence y in rng p by A16, A6, A15; :: thesis: verum

end;

A17: n + k < (n + k) + 1 by NAT_1:13;
then A18: ( Segm (n + k) c= Segm ((n + k) + 1) & n + k in Segm ((n + k) + 1) ) by NAT_1:39, NAT_1:44;
thus for b being bag of n + m holds
( ( b | (n + k) in Support Q & ( for i being Nat st i >= n + k holds
b . i = 0 ) ) iff b in Support p ) :: thesis: ( ( for b being bag of n + m st b in Support p holds
Q . (b | (n + k)) = p . b ) & ( for x being Function of (n + m),L
for y being Function of (n + k),L st x | (n + k) = y holds
eval (p,x) = eval (Q,y) ) )

proof

let b be bag of n + m; :: thesis: ( ( b | (n + k) in Support Q & ( for i being Nat st i >= n + k holds
b . i = 0 ) ) iff b in Support p )
thus ( b | (n + k) in Support Q & ( for i being Nat st i >= n + k holds
b . i = 0 ) implies b in Support p ) :: thesis: ( b in Support p implies ( b | (n + k) in Support Q & ( for i being Nat st i >= n + k holds
b . i = 0 ) ) )

proof

assume A19: ( b | (n + k) in Support Q & ( for i being Nat st i >= n + k holds
b . i = 0 ) ) ; :: thesis: b in Support p
then reconsider b1 = b | (n + k) as Element of Bags (n + k) ;
( q1 . (b1 bag_extend 0) = Q . b1 & Q . b1 <> 0. L ) by Def6, A19, POLYNOM1:def 3;
then A20: b1 bag_extend 0 in Support q1 by A14, POLYNOM1:def 3;
b | ((n + k) + 1) is bag of (n + k) + 1

proof

per cases ( (n + k) + 1 = n + m or (n + k) + 1 < n + m ) by A10, XXREAL_0:1;

suppose (n + k) + 1 = n + m ; :: thesis: b | ((n + k) + 1) is bag of (n + k) + 1

hence b | ((n + k) + 1) is bag of (n + k) + 1 ; :: thesis: verum

end;

suppose (n + k) + 1 < n + m ; :: thesis: b | ((n + k) + 1) is bag of (n + k) + 1

then (n + k) + 1 in Segm (n + m) by NAT_1:44;
hence b | ((n + k) + 1) is bag of (n + k) + 1 by BAGORDER:20; :: thesis: verum

end;

end;

end;

then reconsider bn = b | ((n + k) + 1) as Element of Bags ((n + k) + 1) by PRE_POLY:def 12;
b . (n + k) = 0 by A19;
then ( bn | (n + k) = b1 & bn . (n + k) = 0 ) by FUNCT_1:49, RELAT_1:74, A18;
then A21: bn in Support q1 by A20, HILBASIS:def 1;
for i being Nat st i >= (n + k) + 1 holds
b . i = 0

proof

let i be Nat; :: thesis: ( i >= (n + k) + 1 implies b . i = 0 )
assume i >= (n + k) + 1 ; :: thesis: b . i = 0
then i > n + k by NAT_1:13;
hence b . i = 0 by A19; :: thesis: verum

end;

hence b in Support p by A7, A21; :: thesis: verum

end;

assume A22: b in Support p ; :: thesis: ( b | (n + k) in Support Q & ( for i being Nat st i >= n + k holds
b . i = 0 ) )
then A23: ( b | (n + k1) in Support q & ( for i being Nat st i >= n + k1 holds
b . i = 0 ) ) by A7;
then reconsider bn = b | (n + k1) as Element of Bags ((n + k) + 1) ;
A24: q . bn <> 0. L by A23, POLYNOM1:def 4;
A25: bn . (n + k) = b . (n + k) by A18, FUNCT_1:49;
not n + k in Segm n by NAT_1:11, NAT_1:44;
then A26: not n + k in vars p by A1;
then b . (n + k) = 0 by A22, Def5;
then A27: bn = ((0,(n + k)) -cut bn) bag_extend 0 by A25, HILB10_2:4;
A28: (n + k) -' 0 = (n + k) - 0 ;
then reconsider c = (0,(n + k)) -cut bn as Element of Bags (n + k) by PRE_POLY:def 12;
c = bn | (n + k) by HILB10_2:3, A17;
then A29: c = b | (n + k) by RELAT_1:74, A18;
A30: Q . c = q1 . (c bag_extend 0) by Def6;
for i being Nat st i >= n + k holds
b . i = 0

proof

let i be Nat; :: thesis: ( i >= n + k implies b . i = 0 )
assume i >= n + k ; :: thesis: b . i = 0
then ( i = n + k or i > n + k ) by XXREAL_0:1;
then ( i = n + k or i >= (n + k) + 1 ) by NAT_1:13;
hence b . i = 0 by A26, A22, Def5, A7; :: thesis: verum

end;

hence ( b | (n + k) in Support Q & ( for i being Nat st i >= n + k holds
b . i = 0 ) ) by A30, A27, A28, A24, POLYNOM1:def 4, A29; :: thesis: verum

end;

A31: not n + k in Segm n by NAT_1:11, NAT_1:44;
then A32: not n + k in vars p by A1;
thus for b being bag of n + m st b in Support p holds
Q . (b | (n + k)) = p . b :: thesis: for x being Function of (n + m),L
for y being Function of (n + k),L st x | (n + k) = y holds
eval (p,x) = eval (Q,y)

proof

let b be bag of n + m; :: thesis: ( b in Support p implies Q . (b | (n + k)) = p . b )
assume A33: b in Support p ; :: thesis: Q . (b | (n + k)) = p . b
( b | (n + k1) in Support q & ( for i being Nat st i >= n + k1 holds
b . i = 0 ) ) by A7, A33;
then reconsider bn = b | (n + k1) as Element of Bags ((n + k) + 1) ;
A34: bn . (n + k) = b . (n + k) by A18, FUNCT_1:49;
b . (n + k) = 0 by A33, Def5, A32;
then A35: bn = ((0,(n + k)) -cut bn) bag_extend 0 by A34, HILB10_2:4;
A36: (n + k) -' 0 = (n + k) - 0 ;
then reconsider c = (0,(n + k)) -cut bn as Element of Bags (n + k) by PRE_POLY:def 12;
c = bn | (n + k) by HILB10_2:3, A17;
then A37: c = b | (n + k) by RELAT_1:74, A18;
Q . c = q1 . bn by Def6, A35, A36;
hence Q . (b | (n + k)) = p . b by A37, A33, A8; :: thesis: verum

end;

let x be Function of (n + m),L; :: thesis: for y being Function of (n + k),L st x | (n + k) = y holds
eval (p,x) = eval (Q,y)
let y be Function of (n + k),L; :: thesis: ( x | (n + k) = y implies eval (p,x) = eval (Q,y) )
assume A38: x | (n + k) = y ; :: thesis: eval (p,x) = eval (Q,y)
A39: rng (x | ((n + k) + 1)) c= the carrier of L by RELAT_1:def 19;
(n + k) + 1 c= dom x by A11, FUNCT_2:def 1;
then ( dom (x | ((n + k) + 1)) = (n + k) + 1 & (n + k) + 1 = n + k1 ) by RELAT_1:62;
then reconsider z = x | ((n + k) + 1) as Function of (n + k1),L by A39, FUNCT_2:2;
A40: eval (p,x) = eval (q,z) by A9;
z | (n + k) = y by A38, RELAT_1:74, A18;
hence eval (p,x) = eval (Q,y) by A40, A31, A5, Th51; :: thesis: verum

end;

S₁[ 0 ] from NAT_1:sch 7(A2, A3);
hence ex q being Polynomial of n,L st
( vars q c= n & rng q c= rng p & ( for b being bag of n + m holds
( ( b | n in Support q & ( for i being Nat st i >= n holds
b . i = 0 ) ) iff b in Support p ) ) & ( for b being bag of n + m st b in Support p holds
q . (b | n) = p . b ) & ( for x being Function of (n + m),L
for y being Function of n,L st x | n = y holds
eval (p,x) = eval (q,y) ) ) ; :: thesis: verum