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