let k1 be Integer; 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; ( 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
; ICplusConst (s1,k1) = ICplusConst (s2,k1)
hence
ICplusConst (s1,k1) = ICplusConst (s2,k1)
by A1, SCMPDS_2:def 18; verum