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 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 ;

A: 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
A1: ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) by th3;
A2: degree (a * (z `1)) = degree (z `1) by POLYNOM5:25, A1;
A3: degree (a * (z `2)) = degree (z `2) by POLYNOM5:25, A1;
degree ((NF z) `1) = degree (z `1) by A2, A1, XTUPLE_0:def 2;
hence degree z = max ((degree (z `1)),(degree (z `2))) by A3, A1, XTUPLE_0:def 3; :: thesis: verum

end;

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

assume AS: 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 by defirred;
then consider x being Element of L such that
A1: x is_a_common_root_of z `1 ,z `2 by root2;
A2: ( x is_a_root_of z `1 & x is_a_root_of z `2 ) by A1, root1;
then consider q1 being Polynomial of L such that
A3: z `1 = (rpoly (1,x)) *' q1 by HURWITZ:33;
consider q2 being Polynomial of L such that
A4: z `2 = (rpoly (1,x)) *' q2 by A2, HURWITZ:33;
q2 <> 0_. L by A4, POLYNOM3:34;
then reconsider q2 = q2 as non zero Polynomial of L by defzer;
set zz = [q1,q2];
H1: ( [q1,q2] `1 = q1 & [q1,q2] `2 = q2 ) ;
z = [((rpoly (1,x)) *' ([q1,q2] `1)),((rpoly (1,x)) *' ([q1,q2] `2))] by ttt, A3, A4;
then NF z = NF [q1,q2] by nfequiv;
then degree z = degree [q1,q2] ;
then A8: degree z <= max ((degree q1),(degree q2)) by th1, H1;

now :: thesis: contradiction

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

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

B4: q1 = 0_. L by B0, A3, tt2;
(deg ((rpoly (1,x)) *' q2)) + 0 = (deg (rpoly (1,x))) + (deg q2) by HURWITZ:23
.= 1 + (deg q2) by HURWITZ:27 ;
then C: deg q2 < deg (z `2) by A4, XREAL_1:8;
deg (z `1) <= deg (z `2) by HURWITZ:20, B0;
then B3: max ((deg (z `1)),(deg (z `2))) = deg (z `2) by XXREAL_0:def 10;
deg q1 <= deg q2 by HURWITZ:20, B4;
hence contradiction by B3, C, AS, A8, 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 defzer;

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

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

end;

then reconsider q1 = q1 as non zero Polynomial of L by defzer;
(deg p1) + 0 = (deg (rpoly (1,x))) + (deg q1) by A3, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
then H2: deg q1 < deg p1 by XREAL_1:8;
(deg (z `2)) + 0 = (deg (rpoly (1,x))) + (deg q2) by A4, HURWITZ:23
.= 1 + (deg q2) by HURWITZ:27 ;
then deg q2 < deg (z `2) by XREAL_1:8;
hence contradiction by AS, A8, H2, 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 A; :: thesis: verum