let L be Field; :: thesis:
let z be non zero rational_function of L; :: thesis:
let z1 be rational_function of L; :: thesis:
let z2 be non zero Polynomial of L; :: thesis:
assume H1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; :: thesis:
let g1 be rational_function of L; :: thesis:
let g2 be non zero Polynomial of L; :: thesis:
assume H2: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) ) ; :: thesis:
defpred S₁[ Nat] means for z being non zero rational_function of L st max ((deg (z `1)),(deg (z `2))) = $1 holds
for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1;

now :: thesis:

let z be non zero rational_function of L; :: thesis:
assume max ((deg (z `1)),(deg (z `2))) = 0 ; :: thesis:
then deg (z `2) <= 0 by XXREAL_0:25;
then B: deg (z `2) = 0 ;
let z1 be rational_function of L; :: thesis:
let z2 be non zero Polynomial of L; :: thesis:
assume H1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; :: thesis:
let g1 be rational_function of L; :: thesis:
let g2 be non zero Polynomial of L; :: thesis:
assume H2: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) ) ; :: thesis:

A: now :: thesis:

assume ex x being Element of L st x is_a_root_of z `2 ; :: thesis:
then consider y being Element of L such that
H: y is_a_root_of z `2 ;
eval ((z `2),y) = 0. L by H, POLYNOM5:def 6;
hence contradiction by B, degrat2; :: thesis:

end;

B: now :: thesis:

assume z is reducible ; :: thesis:
then z `1 ,z `2 have_common_roots by defirred;
then consider x being Element of L such that
H: x is_a_common_root_of z `1 ,z `2 by root2;
x is_a_root_of z `2 by H, root1;
hence contradiction by A; :: thesis:

end;

thus g1 = z1 by B, H1, H2, ratfuncNFunique1; :: thesis:

end;

then IA: S₁[ 0 ] ;

IS: now :: thesis:

let n be Nat; :: thesis:
assume IV: S₁[n] ; :: thesis:
for z being non zero rational_function of L st max ((deg (z `1)),(deg (z `2))) = n + 1 holds
for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1

proof

let z be non zero rational_function of L; :: thesis:
assume AS1: max ((deg (z `1)),(deg (z `2))) = n + 1 ; :: thesis:
let z1 be rational_function of L; :: thesis:
let z2 be non zero Polynomial of L; :: thesis:
assume H1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; :: thesis:
consider f being FinSequence of (Polynom-Ring L) such that
H1a: ( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) by H1;
let g1 be rational_function of L; :: thesis:
let g2 be non zero Polynomial of L; :: thesis:
assume H2: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) ) ; :: thesis:
consider g being FinSequence of (Polynom-Ring L) such that
H2a: ( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) by H2;

per cases ;

suppose B: z is irreducible ; :: thesis:

thus g1 = z1 by B, H1, H2, ratfuncNFunique1; :: thesis:

end;

suppose z is reducible ; :: thesis:

then z `1 ,z `2 have_common_roots by defirred;
then consider x being Element of L such that
H: x is_a_common_root_of z `1 ,z `2 by root2;
H3: ( x is_a_root_of z `1 & x is_a_root_of z `2 ) by H, root1;
consider q2 being Polynomial of L such that
HY: z `2 = (rpoly (1,x)) *' q2 by H3, HURWITZ:33;
consider q1 being Polynomial of L such that
HX: z `1 = (rpoly (1,x)) *' q1 by H3, HURWITZ:33;
q2 <> 0_. L by HY, POLYNOM3:34;
then reconsider q2 = q2 as non zero Polynomial of L by defzer;
set q = [q1,q2];
z `1 <> 0_. L by defzerrat;
then q1 <> 0_. L by HX, POLYNOM3:34;
then [q1,q2] `1 <> 0_. L ;
then reconsider q = [q1,q2] as non zero rational_function of L by defzerrat;
AS2: max ((deg (q `1)),(deg (q `2))) = n

proof

A2: deg (z `2) = (deg (rpoly (1,x))) + (deg q2) by HY, HURWITZ:23
.= 1 + (deg q2) by HURWITZ:27 ;
A7: max ((deg (q `1)),(deg (q `2))) = max ((deg q1),(deg (q `2))) by XTUPLE_0:def 2
.= max ((deg q1),(deg q2)) by XTUPLE_0:def 3 ;

per cases by XXREAL_0:16;

suppose A5: max ((deg (z `1)),(deg (z `2))) = deg (z `1) ; :: thesis:

then z `1 <> 0_. L by AS1, HURWITZ:20;
then q1 <> 0_. L by HX, POLYNOM3:34;
then A3: deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by HX, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
deg (z `2) <= n + 1 by AS1, XXREAL_0:25;
then ((deg q2) + 1) - 1 <= (n + 1) - 1 by A2, XREAL_1:9;
hence max ((deg (q `1)),(deg (q `2))) = n by A7, A3, A5, AS1, XXREAL_0:def 10; :: thesis:

end;

suppose A3: max ((deg (z `1)),(deg (z `2))) = deg (z `2) ; :: thesis:

A6: deg (z `1) <= n + 1 by AS1, XXREAL_0:25;

now :: thesis:

per cases ;

suppose q1 = 0_. L ; :: thesis:

hence deg q1 <= deg q2 by HURWITZ:20; :: thesis:

end;

suppose q1 <> 0_. L ; :: thesis:

then deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by HX, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
hence deg q1 <= deg q2 by A6, A3, A2, AS1, XREAL_1:9; :: thesis:

end;

hence max ((deg (q `1)),(deg (q `2))) = n by A7, A2, A3, AS1, XXREAL_0:def 10; :: thesis:

end;

ZZ1: now :: thesis:

let i be Nat; :: thesis:
assume i in dom f ; :: thesis:
then ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) by H1a;
hence ex z being Element of L st f . i = rpoly (1,z) ; :: thesis:

end;

ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )

proof

z2 *' (z1 `1) = (rpoly (1,x)) *' q1 by HX, H1, XTUPLE_0:def 2;
then Z11: rpoly (1,x) divides z2 *' (z1 `1) by HURWITZ:34;
z2 *' (z1 `2) = (rpoly (1,x)) *' q2 by HY, H1, XTUPLE_0:def 3;
then Z11a: rpoly (1,x) divides z2 *' (z1 `2) by HURWITZ:34;

now :: thesis:

per cases by Z11, Z11a, div3;

case rpoly (1,x) divides z2 ; :: thesis:

then eval (z2,x) = 0. L by div1;
then consider i being Nat such that
Z3: ( i in dom f & f . i = rpoly (1,x) ) by div2, H1a, ZZ1;
take i = i; :: thesis:
thus ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by Z3; :: thesis:

end;

case ( rpoly (1,x) divides z1 `1 & rpoly (1,x) divides z1 `2 ) ; :: thesis:

then ( eval ((z1 `1),x) = 0. L & eval ((z1 `2),x) = 0. L ) by div1;
then ( x is_a_root_of z1 `1 & x is_a_root_of z1 `2 ) by POLYNOM5:def 6;
then Z3: x is_a_common_root_of z1 `1 ,z1 `2 by root1;
z1 `1 ,z1 `2 have_no_common_roots by H1, defirred;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by Z3, root2; :: thesis:

end;

hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) ; :: thesis:

end;

then consider i being Nat such that
H5: ( i in dom f & f . i = rpoly (1,x) ) ;

ZZ1a: now :: thesis:

let j be Nat; :: thesis:
assume j in dom g ; :: thesis:
then consider x being Element of L such that
A: ( x is_a_common_root_of z `1 ,z `2 & g . j = rpoly (1,x) ) by H2a;
thus ex z being Element of L st g . j = rpoly (1,z) by A; :: thesis:

end;

ex j being Nat st
( j in dom g & g . j = rpoly (1,x) )

proof

g2 *' (g1 `1) = (rpoly (1,x)) *' q1 by HX, H2, XTUPLE_0:def 2;
then Z11: rpoly (1,x) divides g2 *' (g1 `1) by HURWITZ:34;
g2 *' (g1 `2) = (rpoly (1,x)) *' q2 by HY, H2, XTUPLE_0:def 3;
then Z11a: rpoly (1,x) divides g2 *' (g1 `2) by HURWITZ:34;

now :: thesis:

per cases by Z11, Z11a, div3;

case rpoly (1,x) divides g2 ; :: thesis:

then eval (g2,x) = 0. L by div1;
then consider i being Nat such that
Z3: ( i in dom g & g . i = rpoly (1,x) ) by div2, H2a, ZZ1a;
take i = i; :: thesis:
thus ex j being Nat st
( j in dom g & g . j = rpoly (1,x) ) by Z3; :: thesis:

end;

case ( rpoly (1,x) divides g1 `1 & rpoly (1,x) divides g1 `2 ) ; :: thesis:

then ( eval ((g1 `1),x) = 0. L & eval ((g1 `2),x) = 0. L ) by div1;
then ( x is_a_root_of g1 `1 & x is_a_root_of g1 `2 ) by POLYNOM5:def 6;
then Z3: x is_a_common_root_of g1 `1 ,g1 `2 by root1;
g1 `1 ,g1 `2 have_no_common_roots by H2, defirred;
hence ex j being Nat st
( j in dom g & g . j = rpoly (1,x) ) by Z3, root2; :: thesis:

end;

hence ex j being Nat st
( j in dom g & g . j = rpoly (1,x) ) ; :: thesis:

end;

then consider j being Nat such that
H6: ( j in dom g & g . j = rpoly (1,x) ) ;
reconsider fq = Del (f,i) as FinSequence of (Polynom-Ring L) by FINSEQ_3:105;
reconsider gq = Del (g,j) as FinSequence of (Polynom-Ring L) by FINSEQ_3:105;

X100: now :: thesis:

let k be Nat; :: thesis:
assume H11: k in dom fq ; :: thesis:
consider m being Nat such that
H14: ( len f = m + 1 & len fq = m ) by H5, FINSEQ_3:104;
H14a: k in Seg m by H11, H14, FINSEQ_1:def 3;
Seg m c= Seg (m + 1) by FINSEQ_3:18;
then k in Seg (m + 1) by H14a;
then H13: k in dom f by H14, FINSEQ_1:def 3;
H14b: k <= m by H14a, FINSEQ_1:1;
then H14d: k + 1 <= m + 1 by XREAL_1:6;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (m + 1) by H14d;
then H14c: k + 1 in dom f by H14, FINSEQ_1:def 3;

now :: thesis:

per cases ;

suppose H12: k < i ; :: thesis:

ex y being Element of L st
( y is_a_common_root_of z `1 ,z `2 & f . k = rpoly (1,y) ) by H13, H1a;
hence ex x being Element of L st fq . k = rpoly (1,x) by H12, FINSEQ_3:110; :: thesis:

end;

suppose H12: i <= k ; :: thesis:

ex y being Element of L st
( y is_a_common_root_of z `1 ,z `2 & f . (k + 1) = rpoly (1,y) ) by H1a, H14c;
hence ex x being Element of L st fq . k = rpoly (1,x) by H12, H14b, H5, H14, FINSEQ_3:111; :: thesis:

end;

hence ex x being Element of L st fq . k = rpoly (1,x) ; :: thesis:

end;

X101: now :: thesis:

let k be Nat; :: thesis:
assume H11: k in dom gq ; :: thesis:
consider m being Nat such that
H14: ( len g = m + 1 & len gq = m ) by H6, FINSEQ_3:104;
H14a: k in Seg m by H11, H14, FINSEQ_1:def 3;
Seg m c= Seg (m + 1) by FINSEQ_3:18;
then k in Seg (m + 1) by H14a;
then H13: k in dom g by H14, FINSEQ_1:def 3;
H14b: k <= m by H14a, FINSEQ_1:1;
then H14d: k + 1 <= m + 1 by XREAL_1:6;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (m + 1) by H14d;
then H14c: k + 1 in dom g by H14, FINSEQ_1:def 3;

now :: thesis:

per cases ;

suppose H12: k < j ; :: thesis:

ex y being Element of L st
( y is_a_common_root_of z `1 ,z `2 & g . k = rpoly (1,y) ) by H13, H2a;
hence ex x being Element of L st gq . k = rpoly (1,x) by H12, FINSEQ_3:110; :: thesis:

end;

suppose H12: j <= k ; :: thesis:

ex y being Element of L st
( y is_a_common_root_of z `1 ,z `2 & g . (k + 1) = rpoly (1,y) ) by H2a, H14c;
hence ex x being Element of L st gq . k = rpoly (1,x) by H12, H14b, H6, H14, FINSEQ_3:111; :: thesis:

end;

hence ex x being Element of L st gq . k = rpoly (1,x) ; :: thesis:

end;

reconsider z2q = Product fq as Polynomial of L by POLYNOM3:def 10;
z2q <> 0_. L by X100, div4;
then reconsider z2q = z2q as non zero Polynomial of L by defzer;
reconsider g2q = Product gq as Polynomial of L by POLYNOM3:def 10;
g2q <> 0_. L by X101, div4;
then reconsider g2q = g2q as non zero Polynomial of L by defzer;
H7: Product f = (f /. i) * (Product fq) by H5, del1;
H7a: Product g = (g /. j) * (Product gq) by H6, del1;
Seg (len f) = dom f by FINSEQ_1:def 3;
then ( 1 <= i & i <= len f ) by H5, FINSEQ_1:1;
then f /. i = rpoly (1,x) by H5, FINSEQ_4:15;
then H9: (rpoly (1,x)) *' z2q = Product f by H7, POLYNOM3:def 10;
then H8: (rpoly (1,x)) *' (z2q *' (z1 `1)) = z2 *' (z1 `1) by H1a, POLYNOM3:33
.= (rpoly (1,x)) *' q1 by HX, H1, XTUPLE_0:def 2
.= (rpoly (1,x)) *' (q `1) by XTUPLE_0:def 2 ;
then H8b: z2q *' (z1 `1) = q `1 by thequiv1;
H8a: (rpoly (1,x)) *' (z2q *' (z1 `2)) = z2 *' (z1 `2) by H9, H1a, POLYNOM3:33
.= (rpoly (1,x)) *' q2 by HY, H1, XTUPLE_0:def 3
.= (rpoly (1,x)) *' (q `2) by XTUPLE_0:def 3 ;
then z2q *' (z1 `2) = q `2 by thequiv1;
then I1: q = [(z2q *' (z1 `1)),(z2q *' (z1 `2))] by H8b, MCART_1:8;

I3: now :: thesis:

let k be Element of NAT ; :: thesis:
assume H11: k in dom fq ; :: thesis:
consider m being Nat such that
H14: ( len f = m + 1 & len fq = m ) by H5, FINSEQ_3:104;
H14a: k in Seg m by H11, H14, FINSEQ_1:def 3;
Seg m c= Seg (m + 1) by FINSEQ_3:18;
then k in Seg (m + 1) by H14a;
then H13: k in dom f by H14, FINSEQ_1:def 3;
H14b: k <= m by H14a, FINSEQ_1:1;
then H14d: k + 1 <= m + 1 by XREAL_1:6;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (m + 1) by H14d;
then H14c: k + 1 in dom f by H14, FINSEQ_1:def 3;

now :: thesis:

per cases ;

suppose H12: k < i ; :: thesis:

then H12a: f . k = fq . k by FINSEQ_3:110;
consider y being Element of L such that
H10: ( y is_a_common_root_of z `1 ,z `2 & f . k = rpoly (1,y) ) by H13, H1a;
H25: eval (z2q,y) = 0. L by H12a, H10, H11, X100, div2;
then 0. L = (eval (z2q,y)) * (eval ((z1 `1),y)) by VECTSP_1:7
.= eval ((z2q *' (z1 `1)),y) by POLYNOM4:24
.= eval ((q `1),y) by H8, thequiv1 ;
then A1: y is_a_root_of q `1 by POLYNOM5:def 6;
0. L = (eval (z2q,y)) * (eval ((z1 `2),y)) by VECTSP_1:7, H25
.= eval ((z2q *' (z1 `2)),y) by POLYNOM4:24
.= eval ((q `2),y) by H8a, thequiv1 ;
then y is_a_root_of q `2 by POLYNOM5:def 6;
then y is_a_common_root_of q `1 ,q `2 by A1, root1;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) by H10, H12, FINSEQ_3:110; :: thesis:

end;

suppose H12: i <= k ; :: thesis:

then H12a: f . (k + 1) = fq . k by H14b, H5, H14, FINSEQ_3:111;
consider y being Element of L such that
H10: ( y is_a_common_root_of z `1 ,z `2 & f . (k + 1) = rpoly (1,y) ) by H1a, H14c;
H25: eval (z2q,y) = 0. L by H12a, H10, H11, X100, div2;
then 0. L = (eval (z2q,y)) * (eval ((z1 `1),y)) by VECTSP_1:7
.= eval ((z2q *' (z1 `1)),y) by POLYNOM4:24
.= eval ((q `1),y) by H8, thequiv1 ;
then A1: y is_a_root_of q `1 by POLYNOM5:def 6;
0. L = (eval (z2q,y)) * (eval ((z1 `2),y)) by VECTSP_1:7, H25
.= eval ((z2q *' (z1 `2)),y) by POLYNOM4:24
.= eval ((q `2),y) by H8a, thequiv1 ;
then y is_a_root_of q `2 by POLYNOM5:def 6;
then y is_a_common_root_of q `1 ,q `2 by A1, root1;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) by H10, H12, H14b, H5, H14, FINSEQ_3:111; :: thesis:

end;

hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) ; :: thesis:

end;

Seg (len g) = dom g by FINSEQ_1:def 3;
then ( 1 <= j & j <= len g ) by H6, FINSEQ_1:1;
then g /. j = rpoly (1,x) by H6, FINSEQ_4:15;
then H9: (rpoly (1,x)) *' g2q = Product g by H7a, POLYNOM3:def 10;
then H8: (rpoly (1,x)) *' (g2q *' (g1 `1)) = g2 *' (g1 `1) by H2a, POLYNOM3:33
.= z `1 by H2, XTUPLE_0:def 2
.= (rpoly (1,x)) *' (q `1) by HX, XTUPLE_0:def 2 ;
then H8b: g2q *' (g1 `1) = q `1 by thequiv1;
H8a: (rpoly (1,x)) *' (g2q *' (g1 `2)) = g2 *' (g1 `2) by H9, H2a, POLYNOM3:33
.= z `2 by H2, XTUPLE_0:def 3
.= (rpoly (1,x)) *' (q `2) by HY, XTUPLE_0:def 3 ;
then g2q *' (g1 `2) = q `2 by thequiv1;
then I2: q = [(g2q *' (g1 `1)),(g2q *' (g1 `2))] by H8b, MCART_1:8;

I4: now :: thesis:

let k be Element of NAT ; :: thesis:
assume H11: k in dom gq ; :: thesis:
consider m being Nat such that
H14: ( len g = m + 1 & len gq = m ) by H6, FINSEQ_3:104;
H14a: k in Seg m by H11, H14, FINSEQ_1:def 3;
Seg m c= Seg (m + 1) by FINSEQ_3:18;
then k in Seg (m + 1) by H14a;
then H13: k in dom g by H14, FINSEQ_1:def 3;
H14b: k <= m by H14a, FINSEQ_1:1;
then H14d: k + 1 <= m + 1 by XREAL_1:6;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (m + 1) by H14d;
then H14c: k + 1 in dom g by H14, FINSEQ_1:def 3;

now :: thesis:

per cases ;

suppose H12: k < j ; :: thesis:

then H12a: g . k = gq . k by FINSEQ_3:110;
consider y being Element of L such that
H10: ( y is_a_common_root_of z `1 ,z `2 & g . k = rpoly (1,y) ) by H13, H2a;
H25: eval (g2q,y) = 0. L by H12a, H10, H11, X101, div2;
then 0. L = (eval (g2q,y)) * (eval ((g1 `1),y)) by VECTSP_1:7
.= eval ((g2q *' (g1 `1)),y) by POLYNOM4:24
.= eval ((q `1),y) by H8, thequiv1 ;
then A1: y is_a_root_of q `1 by POLYNOM5:def 6;
0. L = (eval (g2q,y)) * (eval ((g1 `2),y)) by VECTSP_1:7, H25
.= eval ((g2q *' (g1 `2)),y) by POLYNOM4:24
.= eval ((q `2),y) by H8a, thequiv1 ;
then y is_a_root_of q `2 by POLYNOM5:def 6;
then y is_a_common_root_of q `1 ,q `2 by A1, root1;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) by H10, H12, FINSEQ_3:110; :: thesis:

end;

suppose H12: j <= k ; :: thesis:

then H13: g . (k + 1) = gq . k by H14b, H6, H14, FINSEQ_3:111;
consider y being Element of L such that
H10: ( y is_a_common_root_of z `1 ,z `2 & g . (k + 1) = rpoly (1,y) ) by H2a, H14c;
H25: eval (g2q,y) = 0. L by H13, H10, H11, X101, div2;
then 0. L = (eval (g2q,y)) * (eval ((g1 `1),y)) by VECTSP_1:7
.= eval ((g2q *' (g1 `1)),y) by POLYNOM4:24
.= eval ((q `1),y) by H8, thequiv1 ;
then A1: y is_a_root_of q `1 by POLYNOM5:def 6;
0. L = (eval (g2q,y)) * (eval ((g1 `2),y)) by VECTSP_1:7, H25
.= eval ((g2q *' (g1 `2)),y) by POLYNOM4:24
.= eval ((q `2),y) by H8a, thequiv1 ;
then y is_a_root_of q `2 by POLYNOM5:def 6;
then y is_a_common_root_of q `1 ,q `2 by A1, root1;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) by H10, H12, H14b, H6, H14, FINSEQ_3:111; :: thesis:

end;

hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) ; :: thesis:

end;

thus z1 = g1 by H1, H2, I1, I2, I3, I4, AS2, IV; :: thesis:

end;

hence S₁[n + 1] ; :: thesis:

end;

I: for n being Nat holds S₁[n] from NAT_1:sch 2(IA, IS);
max ((deg (z `1)),(deg (z `2))) >= deg (z `2) by XXREAL_0:25;
then max ((deg (z `1)),(deg (z `2))) >= 0 ;
then max ((deg (z `1)),(deg (z `2))) in NAT by INT_1:3;
hence z1 = g1 by I, H1, H2; :: thesis: