let n be Nat; :: thesis: for R being non trivial Ring holds dl. (R,n) = [1,n]
let R be non trivial Ring; :: thesis: dl. (R,n) = [1,n]
thus dl. (R,n) = dl. n by SCMRING3:def 1
.= [1,n] ; :: thesis: verum