let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: Leading-Monomial (1_1 R) = 1_1 R
A1: 1 in dom (0_. R) ;
A2: len (1_1 R) = 1 + 1 by NIVEN:20;
Leading-Monomial (1_1 R) = (0_. R) +* (((len (1_1 R)) -' 1),((1_1 R) . ((len (1_1 R)) -' 1))) by POLYNOM4:11
.= 1_1 R by A2, A1, FUNCT_7:31 ;
hence Leading-Monomial (1_1 R) = 1_1 R ; :: thesis: verum