let s be State of SCMPDS; :: thesis: (IC s) + 1 = ICplusConst (s,1)
consider j being Element of NAT such that
A1: j = IC s and
A2: ICplusConst (s,1) = |.(j + 1).| by SCMPDS_2:def 18;
reconsider mj = IC s as Element of NAT ;
A3: j * 1 >= 0 ;
(IC s) + 1 = |.mj.| + 1 by ABSVALUE:def 1
.= |.mj.| + |.1.| by ABSVALUE:def 1
.= |.(mj + 1).| by A1, A3, ABSVALUE:11 ;
hence (IC s) + 1 = ICplusConst (s,1) by A1, A2; :: thesis: verum