let L be non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis:
let z be rational_function of L; :: thesis:
defpred S₁[ Nat] means for z being rational_function of L st max ((deg (z `1)),(deg (z `2))) = $1 holds
ex z1 being rational_function of L ex 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) ) ) ) );

now :: thesis:

let z be 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 ;

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;

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;

hence ex z1 being rational_function of L ex 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) ) ) ) ) by polynormirred; :: thesis:

end;

then IA: S₁[ 0 ] ;

IS: now :: thesis:

let n be Nat; :: thesis:
assume AS: S₁[n] ; :: thesis:
for z being rational_function of L st max ((deg (z `1)),(deg (z `2))) = n + 1 holds
ex z1 being rational_function of L ex 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) ) ) ) )

proof

let z be rational_function of L; :: thesis:
assume AS1: max ((deg (z `1)),(deg (z `2))) = n + 1 ; :: thesis:

per cases ;

suppose z is irreducible ; :: 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
H2: z `2 = (rpoly (1,x)) *' q2 by H3, HURWITZ:33;
consider q1 being Polynomial of L such that
H1: z `1 = (rpoly (1,x)) *' q1 by H3, HURWITZ:33;
q2 <> 0_. L by H2, POLYNOM3:34;
then reconsider q2 = q2 as non zero Polynomial of L by defzer;
set q = [q1,q2];
max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n

proof

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

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 H1, POLYNOM3:34;
then A3: deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by H1, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
A6: deg (z `2) <= n + 1 by AS1, XXREAL_0:25;
((deg q2) + 1) - 1 <= (n + 1) - 1 by A2, A6, XREAL_1:9;
hence max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n by 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 H1, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
hence deg q1 <= deg q2 by A6, A2, A3, AS1, XREAL_1:9; :: thesis:

end;

hence max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n by A3, A2, AS1, XXREAL_0:def 10; :: thesis:

end;

then consider z1q being rational_function of L, z2q being non zero Polynomial of L such that
IQ: ( [q1,q2] = [(z2q *' (z1q `1)),(z2q *' (z1q `2))] & z1q is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2q = 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 [q1,q2] `1 ,[q1,q2] `2 & f . i = rpoly (1,x) ) ) ) ) by AS;
take z1 = z1q; :: thesis:
set z2 = (rpoly (1,x)) *' z2q;
reconsider z2 = (rpoly (1,x)) *' z2q as non zero Polynomial of L ;
take z2 ; :: thesis:
consider fq being FinSequence of (Polynom-Ring L) such that
IQ2: ( z2q = Product fq & ( for i being Element of NAT st i in dom fq holds
ex x being Element of L st
( x is_a_common_root_of [q1,q2] `1 ,[q1,q2] `2 & fq . i = rpoly (1,x) ) ) ) by IQ;
reconsider rp = rpoly (1,x) as Element of (Polynom-Ring L) by POLYNOM3:def 10;
set f = <*rp*> ^ fq;
IQ3: Product (<*rp*> ^ fq) = rp * (Product fq) by GROUP_4:7
.= z2 by IQ2, POLYNOM3:def 10 ;
IQ4: z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))]

proof

X: q1 = z2q *' (z1q `1) by IQ, XTUPLE_0:def 2;
Z: q2 = z2q *' (z1q `2) by IQ, XTUPLE_0:def 3;
Y: z2 *' (z1 `1) = z `1 by X, H1, POLYNOM3:33;
A: z2 *' (z1 `2) = z `2 by Z, H2, POLYNOM3:33;
thus z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] by Y, A, ttt; :: thesis:

end;

IQ5: now :: thesis:

let i be Element of NAT ; :: thesis:
assume C1: i in dom (<*rp*> ^ fq) ; :: thesis:

now :: thesis:

per cases by C1, FINSEQ_1:25;

suppose C2: i in dom <*rp*> ; :: thesis:

then C3: i in {1} by FINSEQ_1:2, FINSEQ_1:38;
(<*rp*> ^ fq) . i = <*rp*> . i by C2, FINSEQ_1:def 7
.= <*rp*> . 1 by C3, TARSKI:def 1
.= rpoly (1,x) by FINSEQ_1:40 ;
hence ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) by H; :: thesis:

end;

suppose ex n being Nat st
( n in dom fq & i = (len <*rp*>) + n ) ; :: thesis:

then consider n being Nat such that
C2: ( n in dom fq & i = (len <*rp*>) + n ) ;
(<*rp*> ^ fq) . i = fq . n by C2, FINSEQ_1:def 7;
then consider y being Element of L such that
C3: ( y is_a_common_root_of [q1,q2] `1 ,[q1,q2] `2 & (<*rp*> ^ fq) . i = rpoly (1,y) ) by C2, IQ2;
C4: ( y is_a_root_of [q1,q2] `1 & y is_a_root_of [q1,q2] `2 ) by C3, root1;
then C5: 0. L = eval (q1,y) by POLYNOM5:def 6;
C8: eval ((z `1),y) = (eval ((rpoly (1,x)),y)) * (eval (q1,y)) by H1, POLYNOM4:24
.= 0. L by C5, VECTSP_1:7 ;
C6: 0. L = eval (q2,y) by C4, POLYNOM5:def 6;
eval ((z `2),y) = (eval ((rpoly (1,x)),y)) * (eval (q2,y)) by H2, POLYNOM4:24
.= 0. L by C6, VECTSP_1:7 ;
then ( y is_a_root_of z `1 & y is_a_root_of z `2 ) by C8, POLYNOM5:def 6;
then y is_a_common_root_of z `1 ,z `2 by root1;
hence ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) by C3; :: thesis:

end;

hence ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) ; :: thesis:

end;

thus ( 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) ) ) ) ) by IQ, IQ3, IQ4, IQ5; :: 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 ex z1 being rational_function of L ex 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) ) ) ) ) by I; :: thesis: