let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for z being rational_function of L holds degree z <= max ((degree (z `1)),(degree (z `2)))
let z be rational_function of L; :: thesis: degree z <= max ((degree (z `1)),(degree (z `2)))

per cases ( z is zero or not z is zero ) ;

suppose H: z is zero ; :: thesis: degree z <= max ((degree (z `1)),(degree (z `2)))

then A: NF z = 0._ L by defNF
.= [(0_. L),(1_. L)] ;
z `1 = 0_. L by H, defzerrat;
then B: deg (z `1) = - 1 by HURWITZ:20;
E: deg (1_. L) = 1 - 1 by POLYNOM4:4;
deg z = max ((deg (0_. L)),(degree ((NF z) `2))) by A, XTUPLE_0:def 2
.= max ((deg (0_. L)),(deg (1_. L))) by A, XTUPLE_0:def 3
.= max ((- 1),(deg (1_. L))) by HURWITZ:20
.= 0 by E, XXREAL_0:def 10 ;
hence degree z <= max ((degree (z `1)),(degree (z `2))) by B, XXREAL_0:def 10; :: thesis: verum

end;

suppose A: not z is zero ; :: thesis: degree z <= max ((degree (z `1)),(degree (z `2)))

defpred S₁[ Nat] means for z being non zero rational_function of L st max ((degree (z `1)),(degree (z `2))) = $1 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)));

now :: thesis: for z being non zero rational_function of L
for z1 being rational_function of L
for z2 being non zero Polynomial of L
for f being FinSequence of (Polynom-Ring L) st max ((degree (z `1)),(degree (z `2))) = 0 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))

let z be non zero rational_function of L; :: thesis: for z1 being rational_function of L
for z2 being non zero Polynomial of L
for f being FinSequence of (Polynom-Ring L) st max ((degree (z `1)),(degree (z `2))) = 0 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))
let z1 be rational_function of L; :: thesis: for z2 being non zero Polynomial of L
for f being FinSequence of (Polynom-Ring L) st max ((degree (z `1)),(degree (z `2))) = 0 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))
let z2 be non zero Polynomial of L; :: thesis: for f being FinSequence of (Polynom-Ring L) st max ((degree (z `1)),(degree (z `2))) = 0 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))
let f be FinSequence of (Polynom-Ring L); :: thesis: ( max ((degree (z `1)),(degree (z `2))) = 0 implies max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) )
assume AS: max ((degree (z `1)),(degree (z `2))) = 0 ; :: thesis: max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))

now :: thesis: z `1 ,z `2 have_no_common_roots

per cases ( degree (z `1) = 0 or degree (z `2) = 0 ) by AS, XXREAL_0:16;

suppose H: degree (z `1) = 0 ; :: thesis: z `1 ,z `2 have_no_common_roots

now :: thesis: not z `1 ,z `2 have_common_roots

assume z `1 ,z `2 have_common_roots ; :: thesis: contradiction
then consider x being Element of L such that
HH: x is_a_common_root_of z `1 ,z `2 by root2;
x is_a_root_of z `1 by HH, root1;
then z `1 is with_roots by POLYNOM5:def 7;
hence contradiction by HURWITZ:24, H; :: thesis: verum

end;

hence z `1 ,z `2 have_no_common_roots ; :: thesis: verum

end;

suppose H: degree (z `2) = 0 ; :: thesis: z `1 ,z `2 have_no_common_roots

now :: thesis: not z `1 ,z `2 have_common_roots

assume z `1 ,z `2 have_common_roots ; :: thesis: contradiction
then consider x being Element of L such that
HH: x is_a_common_root_of z `1 ,z `2 by root2;
x is_a_root_of z `2 by HH, root1;
then z `2 is with_roots by POLYNOM5:def 7;
hence contradiction by HURWITZ:24, H; :: thesis: verum

end;

hence z `1 ,z `2 have_no_common_roots ; :: thesis: verum

end;

end;

end;

then z is irreducible by defirred;
then degree z = max ((degree (z `1)),(degree (z `2))) by th1a;
hence max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) ; :: thesis: verum

end;

then IA: S₁[ 0 ] ;

IS: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume IV: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: for z being non zero rational_function of L st max ((degree (z `1)),(degree (z `2))) = n + 1 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))

let z be non zero rational_function of L; :: thesis: ( max ((degree (z `1)),(degree (z `2))) = n + 1 implies max ((degree ((NF b₁) `1)),(degree ((NF b<sub>1</sub>) `2))) <= max ((degree (b₁ `1)),(degree (b<sub>1</sub> `2))) )
assume AS: max ((degree (z `1)),(degree (z `2))) = n + 1 ; :: thesis: max ((degree ((NF b₁) `1)),(degree ((NF b<sub>1</sub>) `2))) <= max ((degree (b₁ `1)),(degree (b<sub>1</sub> `2)))

per cases ( z is irreducible or z is reducible ) ;

suppose z is irreducible ; :: thesis: max ((degree ((NF b₁) `1)),(degree ((NF b<sub>1</sub>) `2))) <= max ((degree (b₁ `1)),(degree (b<sub>1</sub> `2)))

then degree z = max ((degree (z `1)),(degree (z `2))) by th1a;
hence max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) ; :: thesis: verum

end;

suppose z is reducible ; :: thesis: max ((degree ((NF b₁) `1)),(degree ((NF b<sub>1</sub>) `2))) <= max ((degree (b₁ `1)),(degree (b<sub>1</sub> `2)))

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;
q1 <> 0_. L by defzerrat, HX, POLYNOM3:34;
then reconsider q1 = q1 as non zero Polynomial of L by defzer;
q2 <> 0_. L by HY, POLYNOM3:34;
then reconsider q2 = q2 as non zero Polynomial of L by defzer;
set q = [q1,q2];

now :: thesis: not [q1,q2] is zero

assume [q1,q2] is zero ; :: thesis: contradiction
then [q1,q2] `1 = 0_. L by defzerrat;
hence contradiction ; :: thesis: verum

end;

then reconsider q = [q1,q2] as non zero rational_function of L ;
z = [((rpoly (1,x)) *' q1),((rpoly (1,x)) *' q2)] by ttt, HX, HY
.= [((rpoly (1,x)) *' (q `1)),((rpoly (1,x)) *' q2)] by XTUPLE_0:def 2
.= [((rpoly (1,x)) *' (q `1)),((rpoly (1,x)) *' (q `2))] by XTUPLE_0:def 3 ;
then HZ: NF z = NF q by nfequiv;
HV: n <= n + 1 by NAT_1:11;
W4: deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by HX, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27
.= 1 + (deg (q `1)) by XTUPLE_0:def 2 ;
deg (z `2) = (deg (rpoly (1,x))) + (deg q2) by HY, HURWITZ:23
.= 1 + (deg q2) by HURWITZ:27
.= 1 + (deg (q `2)) by XTUPLE_0:def 3 ;
then HU: max ((degree (z `1)),(degree (z `2))) = 1 + (max ((degree (q `1)),(degree (q `2)))) by W4, maxx;
then max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (q `1)),(degree (q `2))) by IV, HZ, AS;
hence max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) by HV, HU, AS, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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

end;

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

end;

end;