set f = the Object-Kind of SCMPDS;
set S = the SCMPDS-State;
let k be Integer; :: thesis: ex s being State of SCMPDS st
for d being Int_position holds s . d = k
A1: dom the SCMPDS-State = the carrier of SCMPDS by PARTFUN1:def 2;
A2: dom the Object-Kind of SCMPDS = SCM-Memory by FUNCT_2:def 1;
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 SCMPDS-State +* g;
A4: for x being set st x in dom the Object-Kind of SCMPDS holds
( the SCMPDS-State +* g) . x in the Object-Kind of SCMPDS . x

proof

let x be set ; :: thesis: ( x in dom the Object-Kind of SCMPDS implies ( the SCMPDS-State +* g) . x in the Object-Kind of SCMPDS . x )
assume A5: x in dom the Object-Kind of SCMPDS ; :: thesis: ( the SCMPDS-State +* g) . x in the Object-Kind of SCMPDS . x

per cases ( x in dom g or not x in dom g ) ;

suppose A6: x in dom g ; :: thesis: ( the SCMPDS-State +* g) . x in the Object-Kind of SCMPDS . x

then A7: x in SCM-Data-Loc by FUNCT_2:def 1;
then A8: the Object-Kind of SCMPDS . x = INT by SCMPDS_1:10;
( the SCMPDS-State +* g) . x = g . x by A6, FUNCT_4:13
.= k by A7, FUNCOP_1:7 ;
hence ( the SCMPDS-State +* g) . x in the Object-Kind of SCMPDS . x by A8, INT_1:def 2; :: thesis: verum

end;

suppose not x in dom g ; :: thesis: ( the SCMPDS-State +* g) . x in the Object-Kind of SCMPDS . x

then ( the SCMPDS-State +* g) . x = the SCMPDS-State . x by FUNCT_4:11;
hence ( the SCMPDS-State +* g) . x in the Object-Kind of SCMPDS . x by A5, CARD_3:9; :: thesis: verum

end;

end;

end;

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