theorem :: RATFUNC1:23

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr holds NF (0._ L) = 0._ L by Def17;