A1: now

let x be set ; :: thesis: ( x in dom SCM+FSA-OK implies (s +* (NAT .--> u)) . x in SCM+FSA-OK . x )
assume A2: x in dom SCM+FSA-OK ; :: thesis: (s +* (NAT .--> u)) . x in SCM+FSA-OK . x

now

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

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

{NAT } = dom (NAT .--> u) by FUNCOP_1:19;
then NAT in dom (NAT .--> u) by TARSKI:def 1;
then (s +* (NAT .--> u)) . NAT = (NAT .--> u) . NAT by FUNCT_4:14
.= u by FUNCOP_1:87 ;
hence (s +* (NAT .--> u)) . x in SCM+FSA-OK . x by A3, Th9, ORDINAL1:def 13; :: thesis: verum

end;

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

{NAT } = dom (NAT .--> u) by FUNCOP_1:19;
then not x in dom (NAT .--> u) by A4, TARSKI:def 1;
then (s +* (NAT .--> u)) . x = s . x by FUNCT_4:12;
hence (s +* (NAT .--> u)) . x in SCM+FSA-OK . x by A2, CARD_3:18; :: thesis: verum

end;

end;

end;

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

end;

A5: dom SCM+FSA-OK = SCM+FSA-Memory by FUNCT_2:def 1;
then dom s = SCM+FSA-Memory by CARD_3:18;
then dom (s +* (NAT .--> u)) = SCM+FSA-Memory \/ (dom (NAT .--> u)) by FUNCT_4:def 1
.= SCM+FSA-Memory \/ {NAT } by FUNCOP_1:19
.= dom SCM+FSA-OK by A5, Th5, ZFMISC_1:46 ;
hence s +* (NAT .--> u) is SCM+FSA-State by A1, CARD_3:18; :: thesis: verum