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,L ex q being Polynomial of (n + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for b being bag of n + m holds
( b in Support q iff ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) ) ) ) & ( for b being bag of n + m st b in Support q holds
q . b = p . (b | n) ) & ( for x being Function of n,L
for y being Function of (n + m),L st y | n = x 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,L ex q being Polynomial of (n + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for b being bag of n + m holds
( b in Support q iff ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) ) ) ) & ( for b being bag of n + m st b in Support q holds
q . b = p . (b | n) ) & ( for x being Function of n,L
for y being Function of (n + m),L st y | n = x holds
eval (p,x) = eval (q,y) ) )
let p be Polynomial of n,L; :: thesis: ex q being Polynomial of (n + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for b being bag of n + m holds
( b in Support q iff ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) ) ) ) & ( for b being bag of n + m st b in Support q holds
q . b = p . (b | n) ) & ( for x being Function of n,L
for y being Function of (n + m),L st y | n = x holds
eval (p,x) = eval (q,y) ) )
defpred S₁[ Nat] means ex q being Polynomial of (n + $1),L st
( rng q c= (rng p) \/ {(0. L)} & ( for b being bag of n + $1 holds
( b in Support q iff ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) ) ) ) & ( for b being bag of n + $1 st b in Support q holds
q . b = p . (b | n) ) & ( for x being Function of n,L
for y being Function of (n + $1),L st y | n = x holds
eval (p,x) = eval (q,y) ) );
A1: S₁[ 0 ]

proof

reconsider q = p as Polynomial of (n + 0),L ;
take q ; :: thesis: ( rng q c= (rng p) \/ {(0. L)} & ( for b being bag of n + 0 holds
( b in Support q iff ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) ) ) ) & ( for b being bag of n + 0 st b in Support q holds
q . b = p . (b | n) ) & ( for x being Function of n,L
for y being Function of (n + 0),L st y | n = x holds
eval (p,x) = eval (q,y) ) )
thus rng q c= (rng p) \/ {(0. L)} by XBOOLE_1:7; :: thesis: ( ( for b being bag of n + 0 holds
( b in Support q iff ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) ) ) ) & ( for b being bag of n + 0 st b in Support q holds
q . b = p . (b | n) ) & ( for x being Function of n,L
for y being Function of (n + 0),L st y | n = x holds
eval (p,x) = eval (q,y) ) )
thus for b being bag of n + 0 holds
( b in Support q iff ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) ) ) :: thesis: ( ( for b being bag of n + 0 st b in Support q holds
q . b = p . (b | n) ) & ( for x being Function of n,L
for y being Function of (n + 0),L st y | n = x holds
eval (p,x) = eval (q,y) ) )

proof

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

proof

assume b in Support q ; :: thesis: ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) )
hence b | n in Support p ; :: thesis: for i being Nat st i >= n holds
b . i = 0
let i be Nat; :: thesis: ( i >= n implies b . i = 0 )
assume A2: i >= n ; :: thesis: b . i = 0
( not i in Segm n & Segm n = dom b ) by A2, NAT_1:44, PARTFUN1:def 2;
hence b . i = 0 by FUNCT_1:def 2; :: thesis: verum

end;

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

end;

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

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
set k1 = k + 1;
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider q being Polynomial of (n + k),L such that
A4: rng q c= (rng p) \/ {(0. L)} and
A5: for b being bag of n + k holds
( b in Support q iff ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) ) ) and
A6: for b being bag of n + k st b in Support q holds
q . b = p . (b | n) and
A7: for x being Function of n,L
for y being Function of (n + k),L st y | n = x holds
eval (p,x) = eval (q,y) ;
reconsider P = q extended_by_0 as Polynomial of (n + (k + 1)),L ;
take P ; :: thesis: ( rng P c= (rng p) \/ {(0. L)} & ( for b being bag of n + (k + 1) holds
( b in Support P iff ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) ) ) ) & ( for b being bag of n + (k + 1) st b in Support P holds
P . b = p . (b | n) ) & ( for x being Function of n,L
for y being Function of (n + (k + 1)),L st y | n = x holds
eval (p,x) = eval (P,y) ) )
rng P = (rng q) \/ {(0. L)} by HILB10_2:10;
then rng P c= ((rng p) \/ {(0. L)}) \/ {(0. L)} by A4, XBOOLE_1:13;
hence rng P c= (rng p) \/ {(0. L)} by XBOOLE_1:7, XBOOLE_1:12; :: thesis: ( ( for b being bag of n + (k + 1) holds
( b in Support P iff ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) ) ) ) & ( for b being bag of n + (k + 1) st b in Support P holds
P . b = p . (b | n) ) & ( for x being Function of n,L
for y being Function of (n + (k + 1)),L st y | n = x holds
eval (p,x) = eval (P,y) ) )
A8: ( n + k <= (n + k) + 1 & (n + k) + 1 = n + (k + 1) & n <= n + k ) by NAT_1:11;
A9: Segm n c= Segm (n + k) by NAT_1:39, NAT_1:11;
A10: (n + k) -' 0 = (n + k) - 0 ;
thus for b being bag of n + (k + 1) holds
( b in Support P iff ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) ) ) :: thesis: ( ( for b being bag of n + (k + 1) st b in Support P holds
P . b = p . (b | n) ) & ( for x being Function of n,L
for y being Function of (n + (k + 1)),L st y | n = x holds
eval (p,x) = eval (P,y) ) )

proof

let b be bag of n + (k + 1); :: thesis: ( b in Support P iff ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) ) )
A11: ((0,(n + k)) -cut b) | n = (b | (n + k)) | n by A8, HILB10_2:3
.= b | n by A9, RELAT_1:74 ;

hereby :: thesis: ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) implies b in Support P )

assume A12: b in Support P ; :: thesis: ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) )
then b . (n + k) = 0 by HILB10_2:7;
then A13: (0,(n + k)) -cut b in Support q by A12, HILB10_2:9;
hence b | n in Support p by A5, A11; :: thesis: for i being Nat st i >= n holds
b . i = 0
thus for i being Nat st i >= n holds
b . i = 0 :: thesis: verum

proof

let i be Nat; :: thesis: ( i >= n implies b . i = 0 )
assume A14: i >= n ; :: thesis: b . i = 0

per cases ( i < n + k or i = n + k or i > n + k ) by XXREAL_0:1;

suppose i < n + k ; :: thesis: b . i = 0

then i in Segm (n + k) by NAT_1:44;
then A15: (b | (n + k)) . i = b . i by FUNCT_1:49;
((0,(n + k)) -cut b) . i = 0 by A13, A5, A14;
hence b . i = 0 by A15, A8, HILB10_2:3; :: thesis: verum

end;

suppose i = n + k ; :: thesis: b . i = 0

hence b . i = 0 by A12, HILB10_2:7; :: thesis: verum

end;

suppose i > n + k ; :: thesis: b . i = 0

then i >= (n + k) + 1 by NAT_1:13;
then not i in Segm ((n + k) + 1) by NAT_1:44;
then not i in dom b ;
hence b . i = 0 by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

end;

assume A16: ( b | n in Support p & ( for i being Nat st i >= n holds
b . i = 0 ) ) ; :: thesis: b in Support P
for i being Nat st i >= n holds
((0,(n + k)) -cut b) . i = 0

proof

let i be Nat; :: thesis: ( i >= n implies ((0,(n + k)) -cut b) . i = 0 )
assume A17: i >= n ; :: thesis: ((0,(n + k)) -cut b) . i = 0
A18: ((0,(n + k)) -cut b) . i = (b | (n + k)) . i by A8, HILB10_2:3;

per cases ( i in n + k or not i in n + k ) ;

suppose i in n + k ; :: thesis: ((0,(n + k)) -cut b) . i = 0

then (b | (n + k)) . i = b . i by FUNCT_1:49;
hence ((0,(n + k)) -cut b) . i = 0 by A17, A18, A16; :: thesis: verum

end;

suppose not i in n + k ; :: thesis: ((0,(n + k)) -cut b) . i = 0

then not i in dom ((0,(n + k)) -cut b) by A10;
hence ((0,(n + k)) -cut b) . i = 0 by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

then A19: (0,(n + k)) -cut b in Support q by A10, A5, A16, A11;
b . (n + k) = 0 by A16, NAT_1:11;
hence b in Support P by HILB10_2:9, A19; :: thesis: verum

end;

thus for b being bag of n + (k + 1) st b in Support P holds
P . b = p . (b | n) :: thesis: for x being Function of n,L
for y being Function of (n + (k + 1)),L st y | n = x holds
eval (p,x) = eval (P,y)

proof

let b be bag of n + (k + 1); :: thesis: ( b in Support P implies P . b = p . (b | n) )
assume A20: b in Support P ; :: thesis: P . b = p . (b | n)
A21: ((0,(n + k)) -cut b) | n = (b | (n + k)) | n by A8, HILB10_2:3
.= b | n by A9, RELAT_1:74 ;
b . (n + k) = 0 by A20, HILB10_2:7;
then A22: (0,(n + k)) -cut b in Support q by A20, HILB10_2:9;
(n + k) + 1 = n + (k + 1) ;
then b = ((0,(n + k)) -cut b) bag_extend (b . (n + k)) by HILB10_2:4
.= ((0,(n + k)) -cut b) bag_extend 0 by A20, HILB10_2:7 ;
hence P . b = q . ((0,(n + k)) -cut b) by HILB10_2:6, A10
.= p . (b | n) by A6, A22, A21 ;
:: thesis: verum

end;

let x be Function of n,L; :: thesis: for y being Function of (n + (k + 1)),L st y | n = x holds
eval (p,x) = eval (P,y)
let y be Function of (n + (k + 1)),L; :: thesis: ( y | n = x implies eval (p,x) = eval (P,y) )
assume A23: y | n = x ; :: thesis: eval (p,x) = eval (P,y)
A24: rng ((@ y) | (n + k)) c= the carrier of L by RELAT_1:def 19;
( len (@ y) = n + (k + 1) & n + k < (n + k) + 1 ) by CARD_1:def 7, NAT_1:13;
then dom ((@ y) | (n + k)) = n + k by AFINSQ_1:54;
then reconsider Y = (@ y) | (n + k) as Function of (n + k),L by A24, FUNCT_2:2;
Segm n c= Segm (n + k) by NAT_1:39, NAT_1:11;
then A25: Y | n = x by A23, RELAT_1:74;
thus eval (P,y) = eval (q,Y) by HILB10_2:18
.= eval (p,x) by A7, A25 ; :: thesis: verum

end;

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