A1: now

let x be set ; :: thesis: ( x in dom (SCM-OK R) implies (s +* (NAT .--> u)) . x in (SCM-OK R) . x )
assume A2: x in dom (SCM-OK R) ; :: thesis: (s +* (NAT .--> u)) . x in (SCM-OK R) . x
then A3: x in SCM-Memory by FUNCT_2:def 1;

now

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

suppose A4: x = NAT ; :: thesis: (s +* (NAT .--> u)) . x in (SCM-OK R) . x

{NAT} = dom (NAT .--> u) by FUNCOP_1:13;
then NAT in dom (NAT .--> u) by TARSKI:def 1;
then (s +* (NAT .--> u)) . NAT = (NAT .--> u) . NAT by FUNCT_4:13
.= u by FUNCOP_1:72 ;
then (s +* (NAT .--> u)) . NAT in NAT by ORDINAL1:def 12;
hence (s +* (NAT .--> u)) . x in (SCM-OK R) . x by A3, A4, Th2; :: thesis: verum

end;

suppose A5: x <> NAT ; :: thesis: (s +* (NAT .--> u)) . x in (SCM-OK R) . x

{NAT} = dom (NAT .--> u) by FUNCOP_1:13;
then not x in dom (NAT .--> u) by A5, TARSKI:def 1;
then (s +* (NAT .--> u)) . x = s . x by FUNCT_4:11;
hence (s +* (NAT .--> u)) . x in (SCM-OK R) . x by A2, CARD_3:9; :: thesis: verum

end;

end;

end;

hence (s +* (NAT .--> u)) . x in (SCM-OK R) . x ; :: thesis: verum

end;

A6: dom (SCM-OK R) = SCM-Memory by FUNCT_2:def 1;
then dom s = SCM-Memory by CARD_3:9;
then dom (s +* (NAT .--> u)) = SCM-Memory \/ (dom (NAT .--> u)) by FUNCT_4:def 1
.= SCM-Memory \/ {NAT} by FUNCOP_1:13
.= dom (SCM-OK R) by A6, AMI_2:22, ZFMISC_1:40 ;
hence s +* (NAT .--> u) is SCM-State of R by A1, CARD_3:9; :: thesis: verum