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 A1: ( 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 A2: ( 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 A3: deg (z `2) = 0 ;
let z1 be rational_function of L; :: thesis:
let z2 be non zero Polynomial of L; :: thesis:
assume A4: ( 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 A5: ( 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:

A6: 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
A7: y is_a_root_of z `2 ;
eval ((z `2),y) = 0. L by A7, POLYNOM5:def 7;
hence contradiction by A3, Th8; :: thesis:

end;

A8: now :: thesis:

assume z is reducible ; :: thesis:
then z `1 ,z `2 have_common_roots ;
then consider x being Element of L such that
A9: x is_a_common_root_of z `1 ,z `2 ;
x is_a_root_of z `2 by A9;
hence contradiction by A6; :: thesis:

end;

thus g1 = z1 by A8, A4, A5, Lm2; :: thesis:

end;

then A10: S₁[ 0 ] ;

A11: now :: thesis:

let n be Nat; :: thesis:
assume A12: 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 A13: 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 A14: ( 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
A15: ( 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 A14;
let g1 be rational_function of L; :: thesis:
let g2 be non zero Polynomial of L; :: thesis:
assume A16: ( 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
A17: ( 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 A16;

per cases ;

suppose A18: z is irreducible ; :: thesis:

thus g1 = z1 by A18, A14, A16, Lm2; :: thesis:

end;

suppose z is reducible ; :: thesis:

then z `1 ,z `2 have_common_roots ;
then consider x being Element of L such that
A19: x is_a_common_root_of z `1 ,z `2 ;
A20: ( x is_a_root_of z `1 & x is_a_root_of z `2 ) by A19;
consider q2 being Polynomial of L such that
A21: z `2 = (rpoly (1,x)) *' q2 by A20, HURWITZ:33;
consider q1 being Polynomial of L such that
A22: z `1 = (rpoly (1,x)) *' q1 by A20, HURWITZ:33;
q2 <> 0_. L by A21, POLYNOM3:34;
then reconsider q2 = q2 as non zero Polynomial of L by UPROOTS:def 5;
set q = [q1,q2];
z `1 <> 0_. L by Def9;
then q1 <> 0_. L by A22, POLYNOM3:34;
then [q1,q2] `1 <> 0_. L ;
then reconsider q = [q1,q2] as non zero rational_function of L by Def9;
A23: max ((deg (q `1)),(deg (q `2))) = n

proof

A24: deg (z `2) = (deg (rpoly (1,x))) + (deg q2) by A21, HURWITZ:23
.= 1 + (deg q2) by HURWITZ:27 ;

per cases by XXREAL_0:16;

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

then z `1 <> 0_. L by A13, HURWITZ:20;
then q1 <> 0_. L by A22, POLYNOM3:34;
then A26: deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by A22, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
deg (z `2) <= n + 1 by A13, XXREAL_0:25;
then ((deg q2) + 1) - 1 <= (n + 1) - 1 by A24, XREAL_1:9;
hence max ((deg (q `1)),(deg (q `2))) = n by A26, A25, A13, XXREAL_0:def 10; :: thesis:

end;

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

A28: deg (z `1) <= n + 1 by A13, 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 A22, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
hence deg q1 <= deg q2 by A28, A27, A24, A13, XREAL_1:9; :: thesis:

end;

hence max ((deg (q `1)),(deg (q `2))) = n by A24, A27, A13, XXREAL_0:def 10; :: thesis:

end;

A29: 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 A15;
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 A22, A14;
then A30: rpoly (1,x) divides z2 *' (z1 `1) by HURWITZ:34;
z2 *' (z1 `2) = (rpoly (1,x)) *' q2 by A21, A14;
then A31: rpoly (1,x) divides z2 *' (z1 `2) by HURWITZ:34;

now :: thesis:

per cases by A30, A31, Th10;

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

then eval (z2,x) = 0. L by Th9;
then consider i being Nat such that
A32: ( i in dom f & f . i = rpoly (1,x) ) by Th12, A15, A29;
take i = i; :: thesis:
thus ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by A32; :: 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 Th9;
then ( x is_a_root_of z1 `1 & x is_a_root_of z1 `2 ) by POLYNOM5:def 7;
then A33: x is_a_common_root_of z1 `1 ,z1 `2 ;
z1 `1 ,z1 `2 have_no_common_roots by A14;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by A33; :: 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
A34: ( i in dom f & f . i = rpoly (1,x) ) ;

A35: now :: thesis:

let j be Nat; :: thesis:
assume j in dom g ; :: thesis:
then consider x being Element of L such that
A36: ( x is_a_common_root_of z `1 ,z `2 & g . j = rpoly (1,x) ) by A17;
thus ex z being Element of L st g . j = rpoly (1,z) by A36; :: 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 A22, A16;
then A37: rpoly (1,x) divides g2 *' (g1 `1) by HURWITZ:34;
g2 *' (g1 `2) = (rpoly (1,x)) *' q2 by A21, A16;
then A38: rpoly (1,x) divides g2 *' (g1 `2) by HURWITZ:34;

now :: thesis:

per cases by A37, A38, Th10;

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

then eval (g2,x) = 0. L by Th9;
then consider i being Nat such that
A39: ( i in dom g & g . i = rpoly (1,x) ) by Th12, A17, A35;
take i = i; :: thesis:
thus ex j being Nat st
( j in dom g & g . j = rpoly (1,x) ) by A39; :: 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 Th9;
then ( x is_a_root_of g1 `1 & x is_a_root_of g1 `2 ) by POLYNOM5:def 7;
then A40: x is_a_common_root_of g1 `1 ,g1 `2 ;
g1 `1 ,g1 `2 have_no_common_roots by A16;
hence ex j being Nat st
( j in dom g & g . j = rpoly (1,x) ) by A40; :: 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
A41: ( j in dom g & g . j = rpoly (1,x) ) ;
reconsider fq = Del (f,i) as FinSequence of (Polynom-Ring L) ;
reconsider gq = Del (g,j) as FinSequence of (Polynom-Ring L) ;

A42: now :: thesis:

let k be Nat; :: thesis:
assume A43: k in dom fq ; :: thesis:
consider m being Nat such that
A44: ( len f = m + 1 & len fq = m ) by A34, FINSEQ_3:104;
A45: k in Seg m by A43, A44, FINSEQ_1:def 3;
Seg m c= Seg (m + 1) by FINSEQ_3:18;
then k in Seg (m + 1) by A45;
then A46: k in dom f by A44, FINSEQ_1:def 3;
A47: k <= m by A45, FINSEQ_1:1;
then A48: k + 1 <= m + 1 by XREAL_1:6;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (m + 1) by A48;
then A49: k + 1 in dom f by A44, FINSEQ_1:def 3;

now :: thesis:

per cases ;

suppose A50: 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 A46, A15;
hence ex x being Element of L st fq . k = rpoly (1,x) by A50, FINSEQ_3:110; :: thesis:

end;

suppose A51: 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 A15, A49;
hence ex x being Element of L st fq . k = rpoly (1,x) by A51, A47, A34, A44, FINSEQ_3:111; :: thesis:

end;

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

end;

A52: now :: thesis:

let k be Nat; :: thesis:
assume A53: k in dom gq ; :: thesis:
consider m being Nat such that
A54: ( len g = m + 1 & len gq = m ) by A41, FINSEQ_3:104;
A55: k in Seg m by A53, A54, FINSEQ_1:def 3;
Seg m c= Seg (m + 1) by FINSEQ_3:18;
then k in Seg (m + 1) by A55;
then A56: k in dom g by A54, FINSEQ_1:def 3;
A57: k <= m by A55, FINSEQ_1:1;
then A58: k + 1 <= m + 1 by XREAL_1:6;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (m + 1) by A58;
then A59: k + 1 in dom g by A54, FINSEQ_1:def 3;

now :: thesis:

per cases ;

suppose A60: 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 A56, A17;
hence ex x being Element of L st gq . k = rpoly (1,x) by A60, FINSEQ_3:110; :: thesis:

end;

suppose A61: 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 A17, A59;
hence ex x being Element of L st gq . k = rpoly (1,x) by A61, A57, A41, A54, 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 A42, Th11;
then reconsider z2q = z2q as non zero Polynomial of L by UPROOTS:def 5;
reconsider g2q = Product gq as Polynomial of L by POLYNOM3:def 10;
g2q <> 0_. L by A52, Th11;
then reconsider g2q = g2q as non zero Polynomial of L by UPROOTS:def 5;
A62: Product f = (f /. i) * (Product fq) by A34, Th3;
A63: Product g = (g /. j) * (Product gq) by A41, Th3;
Seg (len f) = dom f by FINSEQ_1:def 3;
then ( 1 <= i & i <= len f ) by A34, FINSEQ_1:1;
then f /. i = rpoly (1,x) by A34, FINSEQ_4:15;
then A64: (rpoly (1,x)) *' z2q = Product f by A62, POLYNOM3:def 10;
then A65: (rpoly (1,x)) *' (z2q *' (z1 `1)) = z2 *' (z1 `1) by A15, POLYNOM3:33
.= (rpoly (1,x)) *' q1 by A22, A14
.= (rpoly (1,x)) *' (q `1) ;
then A66: z2q *' (z1 `1) = q `1 by Th7;
A67: (rpoly (1,x)) *' (z2q *' (z1 `2)) = z2 *' (z1 `2) by A64, A15, POLYNOM3:33
.= (rpoly (1,x)) *' q2 by A21, A14
.= (rpoly (1,x)) *' (q `2) ;
then z2q *' (z1 `2) = q `2 by Th7;
then A68: q = [(z2q *' (z1 `1)),(z2q *' (z1 `2))] by A66;

A69: now :: thesis:

let k be Element of NAT ; :: thesis:
assume A70: k in dom fq ; :: thesis:
consider m being Nat such that
A71: ( len f = m + 1 & len fq = m ) by A34, FINSEQ_3:104;
A72: k in Seg m by A70, A71, FINSEQ_1:def 3;
Seg m c= Seg (m + 1) by FINSEQ_3:18;
then k in Seg (m + 1) by A72;
then A73: k in dom f by A71, FINSEQ_1:def 3;
A74: k <= m by A72, FINSEQ_1:1;
then A75: k + 1 <= m + 1 by XREAL_1:6;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (m + 1) by A75;
then A76: k + 1 in dom f by A71, FINSEQ_1:def 3;

now :: thesis:

per cases ;

suppose A77: k < i ; :: thesis:

then A78: f . k = fq . k by FINSEQ_3:110;
consider y being Element of L such that
A79: ( y is_a_common_root_of z `1 ,z `2 & f . k = rpoly (1,y) ) by A73, A15;
A80: eval (z2q,y) = 0. L by A78, A79, A70, A42, Th12;
then 0. L = (eval (z2q,y)) * (eval ((z1 `1),y))
.= eval ((z2q *' (z1 `1)),y) by POLYNOM4:24
.= eval ((q `1),y) by A65, Th7 ;
then A81: y is_a_root_of q `1 by POLYNOM5:def 7;
0. L = (eval (z2q,y)) * (eval ((z1 `2),y)) by A80
.= eval ((z2q *' (z1 `2)),y) by POLYNOM4:24
.= eval ((q `2),y) by A67, Th7 ;
then y is_a_root_of q `2 by POLYNOM5:def 7;
then y is_a_common_root_of q `1 ,q `2 by A81;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) by A79, A77, FINSEQ_3:110; :: thesis:

end;

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

then A83: f . (k + 1) = fq . k by A74, A34, A71, FINSEQ_3:111;
consider y being Element of L such that
A84: ( y is_a_common_root_of z `1 ,z `2 & f . (k + 1) = rpoly (1,y) ) by A15, A76;
A85: eval (z2q,y) = 0. L by A83, A84, A70, A42, Th12;
then 0. L = (eval (z2q,y)) * (eval ((z1 `1),y))
.= eval ((z2q *' (z1 `1)),y) by POLYNOM4:24
.= eval ((q `1),y) by A65, Th7 ;
then A86: y is_a_root_of q `1 by POLYNOM5:def 7;
0. L = (eval (z2q,y)) * (eval ((z1 `2),y)) by A85
.= eval ((z2q *' (z1 `2)),y) by POLYNOM4:24
.= eval ((q `2),y) by A67, Th7 ;
then y is_a_root_of q `2 by POLYNOM5:def 7;
then y is_a_common_root_of q `1 ,q `2 by A86;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & fq . k = rpoly (1,x) ) by A84, A82, A74, A34, A71, 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 A41, FINSEQ_1:1;
then g /. j = rpoly (1,x) by A41, FINSEQ_4:15;
then A87: (rpoly (1,x)) *' g2q = Product g by A63, POLYNOM3:def 10;
then A88: (rpoly (1,x)) *' (g2q *' (g1 `1)) = g2 *' (g1 `1) by A17, POLYNOM3:33
.= z `1 by A16
.= (rpoly (1,x)) *' (q `1) by A22 ;
then A89: g2q *' (g1 `1) = q `1 by Th7;
A90: (rpoly (1,x)) *' (g2q *' (g1 `2)) = g2 *' (g1 `2) by A87, A17, POLYNOM3:33
.= z `2 by A16
.= (rpoly (1,x)) *' (q `2) by A21 ;
then g2q *' (g1 `2) = q `2 by Th7;
then A91: q = [(g2q *' (g1 `1)),(g2q *' (g1 `2))] by A89;

A92: now :: thesis:

let k be Element of NAT ; :: thesis:
assume A93: k in dom gq ; :: thesis:
consider m being Nat such that
A94: ( len g = m + 1 & len gq = m ) by A41, FINSEQ_3:104;
A95: k in Seg m by A93, A94, FINSEQ_1:def 3;
Seg m c= Seg (m + 1) by FINSEQ_3:18;
then k in Seg (m + 1) by A95;
then A96: k in dom g by A94, FINSEQ_1:def 3;
A97: k <= m by A95, FINSEQ_1:1;
then A98: k + 1 <= m + 1 by XREAL_1:6;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (m + 1) by A98;
then A99: k + 1 in dom g by A94, FINSEQ_1:def 3;

now :: thesis:

per cases ;

suppose A100: k < j ; :: thesis:

then A101: g . k = gq . k by FINSEQ_3:110;
consider y being Element of L such that
A102: ( y is_a_common_root_of z `1 ,z `2 & g . k = rpoly (1,y) ) by A96, A17;
A103: eval (g2q,y) = 0. L by A101, A102, A93, A52, Th12;
then 0. L = (eval (g2q,y)) * (eval ((g1 `1),y))
.= eval ((g2q *' (g1 `1)),y) by POLYNOM4:24
.= eval ((q `1),y) by A88, Th7 ;
then A104: y is_a_root_of q `1 by POLYNOM5:def 7;
0. L = (eval (g2q,y)) * (eval ((g1 `2),y)) by A103
.= eval ((g2q *' (g1 `2)),y) by POLYNOM4:24
.= eval ((q `2),y) by A90, Th7 ;
then y is_a_root_of q `2 by POLYNOM5:def 7;
then y is_a_common_root_of q `1 ,q `2 by A104;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) by A102, A100, FINSEQ_3:110; :: thesis:

end;

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

then A106: g . (k + 1) = gq . k by A97, A41, A94, FINSEQ_3:111;
consider y being Element of L such that
A107: ( y is_a_common_root_of z `1 ,z `2 & g . (k + 1) = rpoly (1,y) ) by A17, A99;
A108: eval (g2q,y) = 0. L by A106, A107, A93, A52, Th12;
then 0. L = (eval (g2q,y)) * (eval ((g1 `1),y))
.= eval ((g2q *' (g1 `1)),y) by POLYNOM4:24
.= eval ((q `1),y) by A88, Th7 ;
then A109: y is_a_root_of q `1 by POLYNOM5:def 7;
0. L = (eval (g2q,y)) * (eval ((g1 `2),y)) by A108
.= eval ((g2q *' (g1 `2)),y) by POLYNOM4:24
.= eval ((q `2),y) by A90, Th7 ;
then y is_a_root_of q `2 by POLYNOM5:def 7;
then y is_a_common_root_of q `1 ,q `2 by A109;
hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & gq . k = rpoly (1,x) ) by A107, A105, A97, A41, A94, 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 A14, A16, A68, A91, A69, A92, A23, A12; :: thesis:

end;

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

end;

A110: for n being Nat holds S₁[n] from NAT_1:sch 2(A10, A11);
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 A110, A1, A2; :: thesis: