let k1 be Integer; :: thesis: for s1, s2 being State of SCMPDS st IC s1 = IC s2 holds
ICplusConst (s1,k1) = ICplusConst (s2,k1)
let s1, s2 be State of SCMPDS; :: thesis: ( IC s1 = IC s2 implies ICplusConst (s1,k1) = ICplusConst (s2,k1) )
A1: ex i being Element of NAT st
( i = IC s1 & ICplusConst (s1,k1) = |.(i + k1).| ) by SCMPDS_2:def 18;
assume IC s1 = IC s2 ; :: thesis: ICplusConst (s1,k1) = ICplusConst (s2,k1)
hence ICplusConst (s1,k1) = ICplusConst (s2,k1) by A1, SCMPDS_2:def 18; :: thesis: verum