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 )
A1: ex m being Element of NAT st
( m = IC s & ICplusConst (s,m2) = abs (m + m2) ) by SCMPDS_2:def 20;
assume IC s = m1 ; :: thesis: ICplusConst (s,m2) = m1 + m2
hence ICplusConst (s,m2) = m1 + m2 by A1, ABSVALUE:def 1; :: thesis: verum