per cases ( not z is zero or z is zero ) ;
suppose not z is zero ; :: thesis: ( NF z is normalized & NF z is irreducible )
then 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 & NF z = NormRatF 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) ) ) ) ) by Def17;
A2: NF z is irreducible by A1, Th20;
(NF z) `2 = ((1. L) / (LC (z1 `2))) * (z1 `2) by A1;
hence ( NF z is normalized & NF z is irreducible ) by A2; :: thesis: verum
end;
suppose z is zero ; :: thesis: ( NF z is normalized & NF z is irreducible )
then NF z = 0._ L by Def17;
hence ( NF z is normalized & NF z is irreducible ) ; :: thesis: verum
end;
end;