A1: dom s = dom the Object-Kind of SCMPDS by CARD_3:18;

A2: now

let x be set ; :: thesis: ( x in dom the Object-Kind of SCMPDS implies (s +* li,k) . b₁ in the Object-Kind of SCMPDS . b₁ )
assume A3: x in dom the Object-Kind of SCMPDS ; :: thesis: (s +* li,k) . b₁ in the Object-Kind of SCMPDS . b₁

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, A3, 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 A3, CARD_3:18; :: thesis: verum

end;

end;

end;

dom (s +* li,k) = dom s by FUNCT_7:32;
hence s +* li,k is State of by A1, A2, CARD_3:18; :: thesis: verum