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