let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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 A1: z is zero ; :: thesis: degree z <= max ((degree (z `1)),(degree (z `2)))

then A2: NF z = 0._ L by Def17
.= [(0_. L),(1_. L)] ;
z `1 = 0_. L by A1;
then A3: deg (z `1) = - 1 by HURWITZ:20;
A4: deg (1_. L) = 1 - 1 by POLYNOM4:4;
deg z = max ((deg (0_. L)),(degree ((NF z) `2))) by A2
.= max ((deg (0_. L)),(deg (1_. L))) by A2
.= max ((- 1),(deg (1_. L))) by HURWITZ:20
.= 0 by A4, XXREAL_0:def 10 ;
hence degree z <= max ((degree (z `1)),(degree (z `2))) by A3, XXREAL_0:def 10; :: thesis: verum

end;

suppose A5: 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 A6: 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 A6, XXREAL_0:16;

suppose A7: 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
A8: x is_a_common_root_of z `1 ,z `2 ;
x is_a_root_of z `1 by A8;
then z `1 is with_roots by POLYNOM5:def 8;
hence contradiction by A7, HURWITZ:24; :: thesis: verum

end;

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

end;

suppose A9: 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
A10: x is_a_common_root_of z `1 ,z `2 ;
x is_a_root_of z `2 by A10;
then z `2 is with_roots by POLYNOM5:def 8;
hence contradiction by A9, HURWITZ:24; :: thesis: verum

end;

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

end;

end;

end;

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

end;

then A11: S₁[ 0 ] ;

A12: 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 A13: 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 A14: 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 Lm6;
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 ;
then consider x being Element of L such that
A15: x is_a_common_root_of z `1 ,z `2 ;
A16: ( x is_a_root_of z `1 & x is_a_root_of z `2 ) by A15;
consider q2 being Polynomial of L such that
A17: z `2 = (rpoly (1,x)) *' q2 by A16, HURWITZ:33;
consider q1 being Polynomial of L such that
A18: z `1 = (rpoly (1,x)) *' q1 by A16, HURWITZ:33;
q1 <> 0_. L by Def9, A18, POLYNOM3:34;
then reconsider q1 = q1 as non zero Polynomial of L by UPROOTS:def 5;
q2 <> 0_. L by A17, POLYNOM3:34;
then reconsider q2 = q2 as non zero Polynomial of L by UPROOTS:def 5;
set q = [q1,q2];
not [q1,q2] is zero ;
then reconsider q = [q1,q2] as non zero rational_function of L ;
z = [((rpoly (1,x)) *' q1),((rpoly (1,x)) *' q2)] by Th19, A18, A17
.= [((rpoly (1,x)) *' (q `1)),((rpoly (1,x)) *' q2)]
.= [((rpoly (1,x)) *' (q `1)),((rpoly (1,x)) *' (q `2))] ;
then A19: NF z = NF q by Th26;
A20: n <= n + 1 by NAT_1:11;
A21: deg (z `1) = (deg (rpoly (1,x))) + (deg q1) by A18, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27
.= 1 + (deg (q `1)) ;
deg (z `2) = (deg (rpoly (1,x))) + (deg q2) by A17, HURWITZ:23
.= 1 + (deg q2) by HURWITZ:27
.= 1 + (deg (q `2)) ;
then A22: max ((degree (z `1)),(degree (z `2))) = 1 + (max ((degree (q `1)),(degree (q `2)))) by A21, Th4;
then max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (q `1)),(degree (q `2))) by A13, A19, A14;
hence max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) by A20, A22, A14, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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

end;

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

end;

end;