let s be State of SCMPDS; :: thesis: for m, n being Nat st IC s = m holds
ICplusConst (s,(n - m)) = n
let m, n be Nat; :: thesis: ( IC s = m implies ICplusConst (s,(n - m)) = n )
ex k being Element of NAT st
( k = IC s & ICplusConst (s,(n - m)) = |.(k + (n - m)).| ) by SCMPDS_2:def 18;
hence ( IC s = m implies ICplusConst (s,(n - m)) = n ) by ABSVALUE:def 1; :: thesis: verum