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