per cases ( not z is zero or z is zero ) ;

suppose not z is zero ; :: thesis: ( ( not z is zero implies ex b₁, z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b₁ = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b₁ being rational_function of L st b₁ = 0._ L ) )

consider z1 being rational_function of L, z2 being non zero Polynomial of L such that
A1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by Th21;
reconsider nfz = NormRatF z1 as rational_function of L ;
ex zz1 being rational_function of L ex zz2 being non zero Polynomial of L st
( nfz = NormRatF zz1 & zz1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( zz2 = Product f & z = [(zz2 *' (zz1 `1)),(zz2 *' (zz1 `2))] & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) by A1;
hence ( ( not z is zero implies ex b₁, z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b₁ = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b₁ being rational_function of L st b₁ = 0._ L ) ) ; :: thesis: verum

end;

suppose z is zero ; :: thesis: ( ( not z is zero implies ex b₁, z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b₁ = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b₁ being rational_function of L st b₁ = 0._ L ) )

hence ( ( not z is zero implies ex b₁, z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b₁ = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b₁ being rational_function of L st b₁ = 0._ L ) ) ; :: thesis: verum

end;

end;