defpred S_{1}[ 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: S_{1}[1]
by lempolybag;

S_{1}[k]
from NAT_1:sch 8(IA, IS);

consider n being Nat such that

H: card (support B) = n ;

then 1 <= n by NAT_1:13;

hence ex b_{1} being Ppoly of R st

( deg b_{1} = card B & ( for a being Element of R holds multiplicity (b_{1},a) = B . a ) )
by H, I; :: thesis: verum

ex p being Ppoly of R st

( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) );

IA: S

IS: now :: thesis: for k being Nat st 1 <= k & S_{1}[k] holds

S_{1}[k + 1]

I:
for k being Nat st 1 <= k holds S

let k be Nat; :: thesis: ( 1 <= k & S_{1}[k] implies S_{1}[k + 1] )

assume AS: 1 <= k ; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume IV: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume AS: 1 <= k ; :: thesis: ( S

assume IV: S

now :: thesis: 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 ) )

hence
Sex 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; :: thesis: ( 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 ; :: thesis: ex p being Ppoly of R st

( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) )

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 ;

( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) ) by A2; :: thesis: verum

end;( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) ) )

assume X: card (support B) = k + 1 ; :: thesis: ex p being Ppoly of R st

( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) )

now :: thesis: ( ( for x being Element of R holds not x in support B ) implies for o being Element of support B holds contradiction )

then consider x being Element of R such that assume A:
for x being Element of R holds not x in support B
; :: thesis: for o being Element of support B holds contradiction

let o be Element of support B; :: thesis: contradiction

end;let o be Element of support B; :: thesis: contradiction

now :: thesis: not support B <> {}

hence
contradiction
by X; :: thesis: verumassume
support B <> {}
; :: thesis: contradiction

then o in support B ;

hence contradiction by A; :: thesis: verum

end;then o in support B ;

hence contradiction by A; :: thesis: verum

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 ;

now :: thesis: for a being Element of R holds multiplicity (q,a) = B . a

hence
ex p being Ppoly of R st let a be Element of R; :: thesis: multiplicity (q,a) = B . a

thus multiplicity (q,a) = (multiplicity (p1,a)) + (multiplicity (p2,a)) by UPROOTS:55

.= ((({x},(B . x)) -bag) . a) + (multiplicity (p2,a)) by A1

.= ((({x},(B . x)) -bag) . a) + (b1 . a) by A5

.= ((({x},(B . x)) -bag) + b1) . a by PRE_POLY:def 5

.= B . a by bb3 ; :: thesis: verum

end;thus multiplicity (q,a) = (multiplicity (p1,a)) + (multiplicity (p2,a)) by UPROOTS:55

.= ((({x},(B . x)) -bag) . a) + (multiplicity (p2,a)) by A1

.= ((({x},(B . x)) -bag) . a) + (b1 . a) by A5

.= ((({x},(B . x)) -bag) + b1) . a by PRE_POLY:def 5

.= B . a by bb3 ; :: thesis: verum

( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) ) by A2; :: thesis: verum

S

consider n being Nat such that

H: card (support B) = n ;

now :: thesis: not n = 0

then
n + 1 > 0 + 1
by XREAL_1:6;assume
n = 0
; :: thesis: contradiction

then support B = {} by H;

hence contradiction by bbag; :: thesis: verum

end;then support B = {} by H;

hence contradiction by bbag; :: thesis: verum

then 1 <= n by NAT_1:13;

hence ex b

( deg b