let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for m being Element of R holds eval ((1_1 R),m) = m
let m be Element of R; :: thesis: eval ((1_1 R),m) = m
A1: len (1_1 R) = 1 + 1 by NIVEN:20;
A2: 1 in dom (0_. R) ;
eval ((1_1 R),m) = eval ((Leading-Monomial (1_1 R)),m) by Th20
.= ((1_1 R) . ((len (1_1 R)) -' 1)) * ((power R) . (m,((len (1_1 R)) -' 1))) by POLYNOM4:22
.= (1. R) * ((power R) . (m,1)) by A1, A2, FUNCT_7:31
.= (power R) . (m,(0 + 1))
.= ((power R) . (m,0)) * m by GROUP_1:def 7
.= (1_ R) * m by GROUP_1:def 7
.= m ;
hence eval ((1_1 R),m) = m ; :: thesis: verum