A1: dom s = the carrier of SCMPDS by PARTFUN1:def 4;

now

let x be set ; :: thesis: ( x in dom (s +* (li,k)) implies (s +* (li,k)) . b₁ in the Object-Kind of SCMPDS . b₁ )
assume x in dom (s +* (li,k)) ; :: thesis: (s +* (li,k)) . b₁ in the Object-Kind of SCMPDS . b₁
then X: x in dom s by A1, PARTFUN1:def 4;

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

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

then A5: the Object-Kind of SCMPDS . x = ObjectKind li
.= INT by SCMPDS_2:13 ;
(s +* (li,k)) . x = k by A1, A4, FUNCT_7:33;
hence (s +* (li,k)) . x in the Object-Kind of SCMPDS . x by A5, INT_1:def 2; :: thesis: verum

end;

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

then (s +* (li,k)) . x = s . x by FUNCT_7:34;
hence (s +* (li,k)) . x in the Object-Kind of SCMPDS . x by X, FUNCT_1:def 20; :: thesis: verum

end;

end;

end;

hence Replace (s,li,k) is PartState of SCMPDS by FUNCT_1:def 20; :: thesis: verum