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 st z is irreducible holds
degree z = max ((degree (z `1)),(degree (z `2)))
let z be non zero rational_function of L; :: 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
H: ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) by th3;
not a is zero by H, STRUCT_0:def 12;
then reconsider az2 = a * (z `2) as non zero Polynomial of L ;
H3: (NF z) `2 = a * (z `2) by H, XTUPLE_0:def 3;
thus degree z = max ((deg (a * (z `1))),(deg (a * (z `2)))) by H, XTUPLE_0:def 2, H3
.= max ((deg (z `1)),(deg az2)) by H, POLYNOM5:25
.= max ((degree (z `1)),(degree (z `2))) by H, POLYNOM5:25 ; :: thesis: verum