A1: now

let x be set ; :: thesis: ( x in dom (s +* (li,k)) implies (s +* (li,k)) . b₁ in the Object-Kind of SCM+FSA . b₁ )
assume x in dom (s +* (li,k)) ; :: thesis: (s +* (li,k)) . b₁ in the Object-Kind of SCM+FSA . b₁
then A2: x in dom s by FUNCT_7:30;

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

suppose A3: x = li ; :: thesis: (s +* (li,k)) . b₁ in the Object-Kind of SCM+FSA . b₁

then A4: the Object-Kind of SCM+FSA . x = ObjectKind li
.= INT by SCMFSA_2:11 ;
(s +* (li,k)) . x = k by A3, A2, FUNCT_7:31;
hence (s +* (li,k)) . x in the Object-Kind of SCM+FSA . x by A4, INT_1:def 2; :: thesis: verum

end;

suppose x <> li ; :: thesis: (s +* (li,k)) . b₁ in the Object-Kind of SCM+FSA . b₁

then (s +* (li,k)) . x = s . x by FUNCT_7:32;
hence (s +* (li,k)) . x in the Object-Kind of SCM+FSA . x by A2, FUNCT_1:def 14; :: thesis: verum

end;

end;

end;

thus s +* (li,k) is State of SCM+FSA by A1, FUNCT_1:def 14; :: thesis: verum