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