let R be domRing; :: thesis: for p being non zero with_roots Polynomial of R ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p )

let p be non zero with_roots Polynomial of R; :: thesis: ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p )

defpred S1[ Nat] means for p being non zero with_roots Polynomial of R st deg p = \$1 holds
ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p );
IA: S1[1]
proof
let p be non zero with_roots Polynomial of R; :: thesis: ( deg p = 1 implies ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p ) )

assume AS: deg p = 1 ; :: thesis: ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p )

consider a being Element of R such that
A1: a is_a_root_of p by POLYNOM5:def 8;
eval (p,a) = 0. R by ;
then consider p1 being Polynomial of R such that
A2: p = (rpoly (1,a)) *' p1 by ;
reconsider q = rpoly (1,a) as Ppoly of R by lemppoly1;
reconsider B = BRoots p as non zero bag of the carrier of R ;
( p1 <> 0_. R & rpoly (1,a) <> 0_. R ) by A2;
then deg p = (deg (rpoly (1,a))) + (deg p1) by
.= 1 + (deg p1) by HURWITZ:27 ;
then reconsider p1 = p1 as non with_roots Polynomial of R by ;
reconsider p1 = p1 as non zero non with_roots Polynomial of R ;
A7: rpoly (1,a) = <%(- a),(1. R)%> by repr;
BRoots p = (BRoots (rpoly (1,a))) + (BRoots p1) by
.= (({a},1) -bag) + (BRoots p1) by
.= (({a},1) -bag) + (EmptyBag the carrier of R) by lemacf1
.= Bag {a} by PRE_POLY:53 ;
then reconsider q = rpoly (1,a) as Ppoly of R, BRoots p by lemacf;
take q ; :: thesis: ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p )

take p1 ; :: thesis: ( p = q *' p1 & Roots q = Roots p )
thus q *' p1 = p by A2; :: thesis:
thus Roots p = () \/ (Roots p1) by
.= Roots q ; :: thesis: verum
end;
IS: now :: thesis: for k being Nat st 1 <= k & S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( 1 <= k & S1[k] implies S1[k + 1] )
assume 1 <= k ; :: thesis: ( S1[k] implies S1[k + 1] )
assume IV: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for p being non zero with_roots Polynomial of R st deg p = k + 1 holds
ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p )
let p be non zero with_roots Polynomial of R; :: thesis: ( deg p = k + 1 implies ex q being Ppoly of R, BRoots q ex r being non with_roots Polynomial of R st
( q = r *' b3 & Roots r = Roots q ) )

assume AS1: deg p = k + 1 ; :: thesis: ex q being Ppoly of R, BRoots q ex r being non with_roots Polynomial of R st
( q = r *' b3 & Roots r = Roots q )

consider a being Element of R such that
A1: a is_a_root_of p by POLYNOM5:def 8;
consider s being Polynomial of R such that
A2: p = (rpoly (1,a)) *' s by ;
reconsider s = s as non zero Polynomial of R by A2;
per cases ;
suppose A4: not s is with_roots ; :: thesis: ex q being Ppoly of R, BRoots q ex r being non with_roots Polynomial of R st
( q = r *' b3 & Roots r = Roots q )

then A5: Roots s = {} ;
reconsider q = rpoly (1,a) as Ppoly of R, Bag {a} by lemacf;
A7: rpoly (1,a) = <%(- a),(1. R)%> by repr;
A6: BRoots p = (BRoots (rpoly (1,a))) + () by
.= (BRoots (rpoly (1,a))) + (EmptyBag the carrier of R) by
.= BRoots (rpoly (1,a)) by PRE_POLY:53
.= Bag {a} by ;
Roots p = () \/ () by
.= Roots q by A5 ;
hence ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p ) by A2, A4, A6; :: thesis: verum
end;
suppose s is with_roots ; :: thesis: ex q being Ppoly of R, BRoots q ex r being non with_roots Polynomial of R st
( q = r *' b3 & Roots r = Roots q )

then reconsider s = s as non zero with_roots Polynomial of R ;
( s <> 0_. R & rpoly (1,a) <> 0_. R ) ;
then deg p = (deg (rpoly (1,a))) + (deg s) by
.= 1 + (deg s) by HURWITZ:27 ;
then consider qs being Ppoly of R, BRoots s, rs being non with_roots Polynomial of R such that
B1: ( s = qs *' rs & Roots qs = Roots s ) by ;
reconsider rs = rs as non zero non with_roots Polynomial of R ;
set q = (rpoly (1,a)) *' qs;
B2: p = ((rpoly (1,a)) *' qs) *' rs by ;
reconsider B = () + () as non zero bag of the carrier of R ;
rpoly (1,a) is Ppoly of R, Bag {a} by lemacf;
then reconsider q = (rpoly (1,a)) *' qs as Ppoly of R,B by lemacf2;
B7: rpoly (1,a) = <%(- a),(1. R)%> by repr;
B4: BRoots p = () + (BRoots rs) by
.= () + (EmptyBag the carrier of R) by lemacf1
.= BRoots q by PRE_POLY:53
.= (BRoots (rpoly (1,a))) + (BRoots qs) by UPROOTS:56
.= () + (BRoots qs) by
.= B by pf2 ;
B3: Roots p = () \/ (Roots rs) by
.= Roots q ;
thus ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p ) by B2, B3, B4; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
I: for k being Nat st 1 <= k holds
S1[k] from NAT_1:sch 8(IA, IS);
K: deg p >= 0 + 1 by ;
p <> 0_. R ;
then deg p is Element of NAT by T8;
then consider d being Nat such that
H: deg p = d ;
thus ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p ) by K, H, I; :: thesis: verum