let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ; :: thesis: NF (1._ L) = 1._ L
set z = 1._ L;
A1: NF (1._ L) = NormRatF (1._ L) by Lm4
.= [(((1. L) / (LC ((1._ L) `2))) * ((1._ L) `1)),(((1. L) / (LC ((1._ L) `2))) * ((1._ L) `2))] ;
(1._ L) `2 is normalized by Def11;
then A2: LC ((1._ L) `2) = 1. L ;
A3: (1. L) / (LC ((1._ L) `2)) = ((LC ((1._ L) `2)) ") * (LC ((1._ L) `2)) by A2
.= 1. L by VECTSP_1:def 10 ;
hence NF (1._ L) = [((1._ L) `1),(((1. L) / (LC ((1._ L) `2))) * ((1._ L) `2))] by A1, POLYNOM5:27
.= [((1._ L) `1),((1._ L) `2)] by A3, POLYNOM5:27
.= 1._ L ;
:: thesis: verum