let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: NF (1._ L) = 1._ L
set z = 1._ L;
B: NF (1._ L) = NormRatF (1._ L) by defnf1a
.= [(((1. L) / (LC ((1._ L) `2))) * ((1._ L) `1)),(((1. L) / (LC ((1._ L) `2))) * ((1._ L) `2))] ;
(1._ L) `2 is normalized by defnorm;
then D: LC ((1._ L) `2) = 1. L by defnormp;
C: (1. L) / (LC ((1._ L) `2)) = 1. L by D, VECTSP_1:def 10;
hence NF (1._ L) = [((1._ L) `1),(((1. L) / (LC ((1._ L) `2))) * ((1._ L) `2))] by B, POLYNOM5:27
.= [((1._ L) `1),((1._ L) `2)] by C, POLYNOM5:27
.= 1._ L by ttt ;
:: thesis: verum