let k be natural number ; :: thesis: Next (il. SCM+FSA ,k) = il. SCM+FSA ,(k + 1)
thus Next (il. SCM+FSA ,k) = Next (insloc k) by Th86
.= k + 1
.= insloc (k + 1)
.= il. SCM+FSA ,(k + 1) by Th86 ; :: thesis: verum