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