set z = [(rpoly (1,x)),(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 ;
then [(rpoly (1,x)),(rpoly (1,x))] `1 ,[(rpoly (1,x)),(rpoly (1,x))] `2 have_common_roots ;
then [(rpoly (1,x)),(rpoly (1,x))] is reducible ;
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 ) ; :: thesis: verum