:: deftheorem Def11 defines normalized RATFUNC1:def 11 :
for L being non trivial right_complementable distributive add-associative right_zeroed unital doubleLoopStr
for z being rational_function of L holds
( z is normalized iff ( z is irreducible & z `2 is normalized ) );