let s be State of ; :: thesis: for m1, m2 being Element of NAT st IC s = inspos m1 holds
ICplusConst s,m2 = inspos (m1 + m2)
let m1, m2 be Element of NAT ; :: thesis: ( IC s = inspos m1 implies ICplusConst s,m2 = inspos (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 = inspos m1 ; :: thesis: ICplusConst s,m2 = inspos (m1 + m2)
hence ICplusConst s,m2 = inspos (m1 + m2) by A1, ABSVALUE:def 1; :: thesis: verum