A1: dom SCMPDS-OK = SCM-Memory by FUNCT_2:def 1;
then dom s = SCM-Memory by CARD_3:18;
then A2: dom (s +* (t .--> u)) = SCM-Memory \/ (dom (t .--> u)) by FUNCT_4:def 1
.= SCM-Memory \/ {t} by FUNCOP_1:19
.= dom SCMPDS-OK by A1, ZFMISC_1:46 ;

now

let x be set ; :: thesis: ( x in dom SCMPDS-OK implies (s +* (t .--> u)) . x in SCMPDS-OK . x )
assume A3: x in dom SCMPDS-OK ; :: thesis: (s +* (t .--> u)) . x in SCMPDS-OK . x

now

per cases ( x = t or x <> t ) ;

suppose A4: x = t ; :: thesis: (s +* (t .--> u)) . x in SCMPDS-OK . x

{t} = dom (t .--> u) by FUNCOP_1:19;
then t in dom (t .--> u) by TARSKI:def 1;
then (s +* (t .--> u)) . t = (t .--> u) . t by FUNCT_4:14
.= u by FUNCOP_1:87 ;
then (s +* (t .--> u)) . t in INT by INT_1:def 2;
hence (s +* (t .--> u)) . x in SCMPDS-OK . x by A4, Th19; :: thesis: verum

end;

suppose A5: x <> t ; :: thesis: (s +* (t .--> u)) . x in SCMPDS-OK . x

{t} = dom (t .--> u) by FUNCOP_1:19;
then not x in dom (t .--> u) by A5, TARSKI:def 1;
then (s +* (t .--> u)) . x = s . x by FUNCT_4:12;
hence (s +* (t .--> u)) . x in SCMPDS-OK . x by A3, CARD_3:18; :: thesis: verum

end;

end;

end;

hence (s +* (t .--> u)) . x in SCMPDS-OK . x ; :: thesis: verum

end;

hence s +* (t .--> u) is SCMPDS-State by A2, CARD_3:18; :: thesis: verum