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 non zero rational_function of L holds
( z is irreducible iff degree z = max ((degree (z `1)),(degree (z `2))) )
let z be non zero rational_function of L; :: thesis: ( z is irreducible iff degree z = max ((degree (z `1)),(degree (z `2))) )
set p1 = z `1 ;
set p2 = z `2 ;

A1: now :: thesis: ( z is irreducible implies degree z = max ((degree (z `1)),(degree (z `2))) )

assume z is irreducible ; :: thesis: degree z = max ((degree (z `1)),(degree (z `2)))
then consider a being Element of L such that
A2: ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) by Th28;
A3: degree (a * (z `1)) = degree (z `1) by A2, POLYNOM5:25;
A4: degree (a * (z `2)) = degree (z `2) by A2, POLYNOM5:25;
degree ((NF z) `1) = degree (z `1) by A3, A2;
hence degree z = max ((degree (z `1)),(degree (z `2))) by A4, A2; :: thesis: verum

end;

now :: thesis: ( degree z = max ((degree (z `1)),(degree (z `2))) implies z is irreducible )

assume A5: degree z = max ((degree (z `1)),(degree (z `2))) ; :: thesis: z is irreducible

now :: thesis: z is irreducible

assume not z is irreducible ; :: thesis: contradiction
then z `1 ,z `2 have_a_common_root ;
then consider x being Element of L such that
A6: x is_a_common_root_of z `1 ,z `2 ;
A7: ( x is_a_root_of z `1 & x is_a_root_of z `2 ) by A6;
then consider q1 being Polynomial of L such that
A8: z `1 = (rpoly (1,x)) *' q1 by HURWITZ:33;
consider q2 being Polynomial of L such that
A9: z `2 = (rpoly (1,x)) *' q2 by A7, HURWITZ:33;
q2 <> 0_. L by A9, POLYNOM3:34;
then reconsider q2 = q2 as non zero Polynomial of L by UPROOTS:def 5;
set zz = [q1,q2];
A10: ( [q1,q2] `1 = q1 & [q1,q2] `2 = q2 ) ;
z = [((rpoly (1,x)) *' ([q1,q2] `1)),((rpoly (1,x)) *' ([q1,q2] `2))] by Th19, A8, A9;
then NF z = NF [q1,q2] by Th26;
then degree z = degree [q1,q2] ;
then A11: degree z <= max ((degree q1),(degree q2)) by Th29, A10;

now :: thesis: contradiction

per cases ( z `1 = 0_. L or z `1 <> 0_. L ) ;

suppose A12: z `1 = 0_. L ; :: thesis: contradiction

A13: q1 = 0_. L by A12, A8, Lm5;
(deg ((rpoly (1,x)) *' q2)) + 0 = (deg (rpoly (1,x))) + (deg q2) by HURWITZ:23
.= 1 + (deg q2) by HURWITZ:27 ;
then A14: deg q2 < deg (z `2) by A9, XREAL_1:8;
deg (z `1) <= deg (z `2) by A12, HURWITZ:20;
then A15: max ((deg (z `1)),(deg (z `2))) = deg (z `2) by XXREAL_0:def 10;
deg q1 <= deg q2 by A13, HURWITZ:20;
hence contradiction by A15, A14, A5, A11, XXREAL_0:def 10; :: thesis: verum

end;

suppose z `1 <> 0_. L ; :: thesis: contradiction

then reconsider p1 = z `1 as non zero Polynomial of L by UPROOTS:def 5;

now :: thesis: not q1 = 0_. L

assume q1 = 0_. L ; :: thesis: contradiction
then p1 = 0_. L by A8, POLYNOM3:34;
hence contradiction ; :: thesis: verum

end;

then reconsider q1 = q1 as non zero Polynomial of L by UPROOTS:def 5;
(deg p1) + 0 = (deg (rpoly (1,x))) + (deg q1) by A8, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
then A16: deg q1 < deg p1 by XREAL_1:8;
(deg (z `2)) + 0 = (deg (rpoly (1,x))) + (deg q2) by A9, HURWITZ:23
.= 1 + (deg q2) by HURWITZ:27 ;
then deg q2 < deg (z `2) by XREAL_1:8;
hence contradiction by A5, A11, A16, XXREAL_0:27; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence z is irreducible ; :: thesis: verum

end;

hence ( z is irreducible iff degree z = max ((degree (z `1)),(degree (z `2))) ) by A1; :: thesis: verum