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 rational_function of L holds NF (NF z) = NF z
let z be rational_function of L; :: thesis: NF (NF z) = NF z
set nfz = NF z;

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

suppose z is zero ; :: thesis: NF (NF z) = NF z

then A1: NF z = 0._ L by Def17;
thus NF (NF z) = NF z by A1, Def17; :: thesis: verum

end;

suppose A2: not z is zero ; :: thesis: NF (NF z) = NF z

A3: 1. L <> 0. L ;
A4: NF (NF z) = NormRatF (NF z) by A2, Lm4
.= [(((1. L) / (LC ((NF z) `2))) * ((NF z) `1)),(((1. L) / (LC ((NF z) `2))) * ((NF z) `2))] ;
(NF z) `2 is normalized by Def11;
then A5: LC ((NF z) `2) = 1. L ;
A6: (1. L) / (LC ((NF z) `2)) = ((LC ((NF z) `2)) ") * (LC ((NF z) `2)) by A5
.= 1. L by VECTSP_1:def 10, A3 ;
then NF (NF z) = [((NF z) `1),(((1. L) / (LC ((NF z) `2))) * ((NF z) `2))] by A4, POLYNOM5:27
.= [((NF z) `1),((NF z) `2)] by A6, POLYNOM5:27
.= NF z by Th19 ;
hence NF (NF z) = NF z ; :: thesis: verum

end;

end;