set f = the Object-Kind of SCMPDS ;
consider S being 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 S = the carrier of SCMPDS by PARTFUN1:def 4;
A2: dom the Object-Kind of SCMPDS = SCM-Memory by FUNCT_2:def 1;
consider g being Function of SCM-Data-Loc ,INT such that
A3: for x being Element of SCM-Data-Loc holds g . x = k by Th72;
set t = S +* g;
A4: for x being set st x in dom the Object-Kind of SCMPDS holds
(S +* g) . x in the Object-Kind of SCMPDS . x

proof

let x be set ; :: thesis: ( x in dom the Object-Kind of SCMPDS implies (S +* g) . x in the Object-Kind of SCMPDS . x )
assume A5: x in dom the Object-Kind of SCMPDS ; :: thesis: (S +* 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: (S +* 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:21;
(S +* g) . x = g . x by A6, FUNCT_4:14
.= k by A3, A7 ;
hence (S +* 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: (S +* g) . x in the Object-Kind of SCMPDS . x

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

end;

end;

end;

dom (S +* g) = (dom S) \/ (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 = S +* g as State of SCMPDS by A2, A4, FUNCT_1:def 20, PARTFUN1:def 4, 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:14
.= k by A3 ;
:: thesis: verum