let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 A: NF z = 0._ L by defNF;
thus NF (NF z) = NF z by A, defNF; :: thesis: verum

end;

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

H: 1. L <> 0. L ;
B: NF (NF z) = NormRatF (NF z) by A, defnf1a
.= [(((1. L) / (LC ((NF z) `2))) * ((NF z) `1)),(((1. L) / (LC ((NF z) `2))) * ((NF z) `2))] ;
(NF z) `2 is normalized by defnorm;
then D: LC ((NF z) `2) = 1. L by defnormp;
C: (1. L) / (LC ((NF z) `2)) = 1. L by H, D, VECTSP_1:def 10;
then NF (NF z) = [((NF z) `1),(((1. L) / (LC ((NF z) `2))) * ((NF z) `2))] by B, POLYNOM5:27
.= [((NF z) `1),((NF z) `2)] by C, POLYNOM5:27
.= NF z by ttt ;
hence NF (NF z) = NF z ; :: thesis: verum

end;

end;