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