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