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 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
A1: ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) by Th28;
not a is zero by A1;
then reconsider az2 = a * (z `2) as non zero Polynomial of L ;
thus degree z = max ((deg (a * (z `1))),(deg (a * (z `2)))) by A1
.= max ((deg (z `1)),(deg az2)) by A1, POLYNOM5:25
.= max ((degree (z `1)),(degree (z `2))) by A1, POLYNOM5:25 ; :: thesis: verum