set f = the_Values_of SCMPDS;
set S = the SCM-State;
let k be Integer; :: thesis:
the SCM-State is SCM-Memory -defined total Function by AMI_2:29;
then A1: dom the SCM-State = the carrier of SCMPDS by PARTFUN1:def 2;
A2: dom (the_Values_of SCMPDS) = SCM-Memory by PARTFUN1:def 2;
k in INT by INT_1:def 2;
then reconsider g = SCM-Data-Loc --> k as Function of SCM-Data-Loc,INT by FUNCOP_1:45;
set t = the SCM-State +* g;
A3: for x being object st x in dom (the_Values_of SCMPDS) holds
( the SCM-State +* g) . x in (the_Values_of SCMPDS) . x

let x be object ; :: thesis:
assume A4: x in dom (the_Values_of SCMPDS) ; :: thesis:

suppose A5: x in dom g ; :: thesis:

then A6: x in SCM-Data-Loc ;
then A7: (the_Values_of SCMPDS) . x = INT by AMI_2:8;
( the SCM-State +* g) . x = g . x by A5, FUNCT_4:13
.= k by A6, FUNCOP_1:7 ;
hence ( the SCM-State +* g) . x in (the_Values_of SCMPDS) . x by A7, INT_1:def 2; :: thesis:

end;

suppose not x in dom g ; :: thesis:

then ( the SCM-State +* g) . x = the SCM-State . x by FUNCT_4:11;
hence ( the SCM-State +* g) . x in (the_Values_of SCMPDS) . x by A4, CARD_3:9; :: thesis:

end;

end;

end;

dom ( the SCM-State +* g) = (dom the SCM-State) \/ (dom g) by FUNCT_4:def 1
.= SCM-Memory \/ (dom g) by A1
.= SCM-Memory \/ SCM-Data-Loc
.= SCM-Memory by XBOOLE_1:12 ;
then reconsider s = the SCM-State +* g as State of SCMPDS by A2, A3, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;
take s ; :: thesis:
let d be Int_position; :: thesis:
reconsider D = d as Element of SCM-Data-Loc by AMI_2:def 16;
D in dom g ;
hence s . d = g . D by FUNCT_4:13
.= k ;
:: thesis: