defpred S₁[ 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] by lempolybag;

IS: now :: thesis: for k being Nat st 1 <= k & S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( 1 <= k & S₁[k] implies S₁[k + 1] )
assume AS: 1 <= k ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]

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 ) )

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 ) )

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

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

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

assume support B <> {} ; :: thesis: contradiction
then o in support B ;
hence contradiction by A; :: thesis: verum

end;

hence contradiction by X; :: thesis: verum

end;

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 ;

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

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;

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; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(IA, IS);
consider n being Nat such that
H: card (support B) = n ;

now :: thesis: not n = 0

assume n = 0 ; :: thesis: contradiction
then support B = {} by H;
hence contradiction by bbag; :: thesis: verum

end;

then n + 1 > 0 + 1 by XREAL_1:6;
then 1 <= n by NAT_1:13;
hence ex b₁ being Ppoly of R st
( deg b₁ = card B & ( for a being Element of R holds multiplicity (b₁,a) = B . a ) ) by H, I; :: thesis: verum