set z = [(rpoly (1,x)),(rpoly (1,x))];
C: [(rpoly (1,x)),(rpoly (1,x))] `1 = rpoly (1,x) ;
x is_a_root_of rpoly (1,x) by HURWITZ:30;
then x is_a_root_of [(rpoly (1,x)),(rpoly (1,x))] `1 ;
then x is_a_common_root_of [(rpoly (1,x)),(rpoly (1,x))] `1 ,[(rpoly (1,x)),(rpoly (1,x))] `2 by root1;
then [(rpoly (1,x)),(rpoly (1,x))] `1 ,[(rpoly (1,x)),(rpoly (1,x))] `2 have_common_roots by root2;
then [(rpoly (1,x)),(rpoly (1,x))] is reducible by defirred;
hence for b₁ being rational_function of L st b₁ = [(rpoly (1,x)),(rpoly (1,x))] holds
( not b₁ is irreducible & not b₁ is zero ) by C, defzerrat; :: thesis: verum