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