let k be natural number ; :: thesis: for R being good Ring holds il. (SCM R),k = k
let R be good Ring; :: thesis: il. (SCM R),k = k
thus il. (SCM R),k = il. k by SCMRING3:66
.= k ; :: thesis: verum