A1: now :: thesis: for x being object st x in dom (SCM*-VAL * SCM+FSA-OK) holds
(s +* (t .--> u)) . x in (SCM*-VAL * SCM+FSA-OK) . x

let x be object ; :: thesis: ( x in dom (SCM*-VAL * SCM+FSA-OK) implies (s +* (t .--> u)) . b₁ in (SCM*-VAL * SCM+FSA-OK) . b₁ )
assume A2: x in dom (SCM*-VAL * SCM+FSA-OK) ; :: thesis: (s +* (t .--> u)) . b₁ in (SCM*-VAL * SCM+FSA-OK) . b₁

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

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

t in dom (t .--> u) by TARSKI:def 1;
then (s +* (t .--> u)) . t = (t .--> u) . t by FUNCT_4:13
.= u by FUNCOP_1:72 ;
then (s +* (t .--> u)) . t in INT * by FINSEQ_1:def 11;
hence (s +* (t .--> u)) . x in (SCM*-VAL * SCM+FSA-OK) . x by A3, Th6; :: thesis: verum

end;

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

not x in dom (t .--> u) by A4, TARSKI:def 1;
then (s +* (t .--> u)) . x = s . x by FUNCT_4:11;
hence (s +* (t .--> u)) . x in (SCM*-VAL * SCM+FSA-OK) . x by A2, CARD_3:9; :: thesis: verum

end;

end;

end;

A5: dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then dom s = SCM+FSA-Memory by CARD_3:9;
then dom (s +* (t .--> u)) = SCM+FSA-Memory \/ (dom (t .--> u)) by FUNCT_4:def 1
.= SCM+FSA-Memory \/ {t}
.= dom (SCM*-VAL * SCM+FSA-OK) by A5, ZFMISC_1:40 ;
hence s +* (t .--> u) is SCM+FSA-State by A1, CARD_3:9; :: thesis: verum