let L be non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative 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 A1: deg (z `2) = 0 ;

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

end;

now :: thesis:

assume z is reducible ; :: thesis:
then z `1 ,z `2 have_common_roots ;
then consider x being Element of L such that
A4: x is_a_common_root_of z `1 ,z `2 ;
x is_a_root_of z `2 by A4;
hence contradiction by A2; :: 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 Lm1; :: thesis:

end;

then A5: S₁[ 0 ] ;

A6: now :: thesis:

let n be Nat; :: thesis:
assume A7: 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 A8: 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 ;
then consider x being Element of L such that
A9: x is_a_common_root_of z `1 ,z `2 ;
A10: ( x is_a_root_of z `1 & x is_a_root_of z `2 ) by A9;
consider q2 being Polynomial of L such that
A11: z `2 = (rpoly (1,x)) *' q2 by A10, HURWITZ:33;
consider q1 being Polynomial of L such that
A12: z `1 = (rpoly (1,x)) *' q1 by A10, HURWITZ:33;
q2 <> 0_. L by A11, POLYNOM3:34;
then reconsider q2 = q2 as non zero Polynomial of L by UPROOTS:def 5;
set q = [q1,q2];
max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n

proof

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

per cases by XXREAL_0:16;

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

then z `1 <> 0_. L by A8, HURWITZ:20;
then q1 <> 0_. L by A12, POLYNOM3:34;
then A15: deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by A12, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
A16: deg (z `2) <= n + 1 by A8, XXREAL_0:25;
((deg q2) + 1) - 1 <= (n + 1) - 1 by A13, A16, XREAL_1:9;
hence max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n by A15, A14, A8, XXREAL_0:def 10; :: thesis:

end;

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

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

end;

hence max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = n by A17, A13, A8, XXREAL_0:def 10; :: thesis:

end;

then consider z1q being rational_function of L, z2q being non zero Polynomial of L such that
A19: ( [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 A7;
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
A20: ( 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 A19;
reconsider rp = rpoly (1,x) as Element of (Polynom-Ring L) by POLYNOM3:def 10;
set f = <*rp*> ^ fq;
A21: Product (<*rp*> ^ fq) = rp * (Product fq) by GROUP_4:7
.= z2 by A20, POLYNOM3:def 10 ;
A22: z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))]

proof

A23: q1 = z2q *' (z1q `1) by A19, XTUPLE_0:def 2;
A24: q2 = z2q *' (z1q `2) by A19, XTUPLE_0:def 3;
A25: z2 *' (z1 `1) = z `1 by A23, A12, POLYNOM3:33;
A26: z2 *' (z1 `2) = z `2 by A24, A11, POLYNOM3:33;
thus z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] by A25, A26, Th19; :: thesis:

end;

A27: now :: thesis:

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

now :: thesis:

per cases by A28, FINSEQ_1:25;

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

then A30: i in {1} by FINSEQ_1:2, FINSEQ_1:38;
(<*rp*> ^ fq) . i = <*rp*> . i by A29, FINSEQ_1:def 7
.= <*rp*> . 1 by A30, TARSKI:def 1
.= rpoly (1,x) ;
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 A9; :: thesis:

end;

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

then consider n being Nat such that
A31: ( n in dom fq & i = (len <*rp*>) + n ) ;
(<*rp*> ^ fq) . i = fq . n by A31, FINSEQ_1:def 7;
then consider y being Element of L such that
A32: ( y is_a_common_root_of [q1,q2] `1 ,[q1,q2] `2 & (<*rp*> ^ fq) . i = rpoly (1,y) ) by A31, A20;
A33: ( y is_a_root_of [q1,q2] `1 & y is_a_root_of [q1,q2] `2 ) by A32;
then A34: 0. L = eval (q1,y) by POLYNOM5:def 7;
A35: eval ((z `1),y) = (eval ((rpoly (1,x)),y)) * (eval (q1,y)) by A12, POLYNOM4:24
.= 0. L by A34 ;
A36: 0. L = eval (q2,y) by A33, POLYNOM5:def 7;
eval ((z `2),y) = (eval ((rpoly (1,x)),y)) * (eval (q2,y)) by A11, POLYNOM4:24
.= 0. L by A36 ;
then ( y is_a_root_of z `1 & y is_a_root_of z `2 ) by A35, POLYNOM5:def 7;
then y is_a_common_root_of z `1 ,z `2 ;
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 A32; :: 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 A19, A21, A22, A27; :: thesis:

end;

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

end;

A37: for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A6);
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 A37; :: thesis: