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