defpred S1[ Nat] means for B being non zero bag of the carrier of R st card (support B) = $1 holds
ex p being Ppoly of R st
( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) );
IA:
S1[1]
by lempolybag;
IS:
now for k being Nat st 1 <= k & S1[k] holds
S1[k + 1]let k be
Nat;
( 1 <= k & S1[k] implies S1[k + 1] )assume AS:
1
<= k
;
( S1[k] implies S1[k + 1] )assume IV:
S1[
k]
;
S1[k + 1]now for B being non zero bag of the carrier of R st card (support B) = k + 1 holds
ex p being Ppoly of R st
( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) )let B be non
zero bag of the
carrier of
R;
( card (support B) = k + 1 implies ex p being Ppoly of R st
( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) ) )assume X:
card (support B) = k + 1
;
ex p being Ppoly of R st
( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) )then consider x being
Element of
R such that A:
x in support B
;
H1:
for
o being
object st
o in {x} holds
o in support B
by A, TARSKI:def 1;
set b = (
{x},
(B . x))
-bag ;
set b1 =
B \ x;
B . x <> 0
by A, PRE_POLY:def 7;
then
support (({x},(B . x)) -bag) = {x}
by UPROOTS:8;
then
card (support (({x},(B . x)) -bag)) = 1
by CARD_1:30;
then consider p1 being
Ppoly of
R such that A1:
(
deg p1 = card (({x},(B . x)) -bag) & ( for
a being
Element of
R holds
multiplicity (
p1,
a)
= (({x},(B . x)) -bag) . a ) )
by lempolybag;
A3:
card (support (B \ x)) =
card ((support B) \ {x})
by bb3a
.=
(card (support B)) - (card {x})
by TARSKI:def 3, H1, CARD_2:44
.=
(card (support B)) - 1
by CARD_1:30
;
then
support (B \ x) <> {}
by X, AS;
then reconsider b1 =
B \ x as non
zero bag of the
carrier of
R by bbag;
consider p2 being
Ppoly of
R such that A5:
(
deg p2 = card b1 & ( for
a being
Element of
R holds
multiplicity (
p2,
a)
= b1 . a ) )
by A3, X, IV;
reconsider q =
p1 *' p2 as
Ppoly of
R by lemppoly3;
(
p1 <> 0_. R &
p2 <> 0_. R )
;
then A2:
deg q =
(deg p1) + (deg p2)
by HURWITZ:23
.=
card ((({x},(B . x)) -bag) + b1)
by A1, A5, UPROOTS:15
.=
card B
by bb3
;
hence
ex
p being
Ppoly of
R st
(
deg p = card B & ( for
a being
Element of
R holds
multiplicity (
p,
a)
= B . a ) )
by A2;
verum end; hence
S1[
k + 1]
;
verum end;
I:
for k being Nat st 1 <= k holds
S1[k]
from NAT_1:sch 8(IA, IS);
consider n being Nat such that
H:
card (support B) = n
;
then
n + 1 > 0 + 1
by XREAL_1:6;
then
1 <= n
by NAT_1:13;
hence
ex b1 being Ppoly of R st
( deg b1 = card B & ( for a being Element of R holds multiplicity (b1,a) = B . a ) )
by H, I; verum