A1: dom s = the carrier of SCM+FSA by PARTFUN1:def 4;
B1: dom (s +* (li,k)) = dom s by FUNCT_7:32;

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 X: x in dom s by B1;

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

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

then A5: the Object-Kind of SCM+FSA . x = ObjectKind li
.= INT by SCMFSA_2:26 ;
(s +* (li,k)) . x = k by A4, X, FUNCT_7:33;
hence (s +* (li,k)) . x in the Object-Kind of SCM+FSA . x by A5, 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:34;
hence (s +* (li,k)) . x in the Object-Kind of SCM+FSA . x by X, FUNCT_1:def 20; :: thesis: verum

end;

end;

end;

then Y: s +* (li,k) is the Object-Kind of SCM+FSA -compatible by FUNCT_1:def 20;
dom (s +* (li,k)) = dom s by FUNCT_7:32;
hence s +* (li,k) is State of SCM+FSA by A1, Y, PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum