A1: dom s = the carrier of SCMPDS by PARTFUN1:def 2;
now :: thesis: for x being object st x in dom (s +* (li,k)) holds
(s +* (li,k)) . x in (the_Values_of SCMPDS) . x
let x be object ; :: thesis: ( x in dom (s +* (li,k)) implies (s +* (li,k)) . b1 in (the_Values_of SCMPDS) . b1 )
assume x in dom (s +* (li,k)) ; :: thesis: (s +* (li,k)) . b1 in (the_Values_of SCMPDS) . b1
then A2: x in dom s by A1, PARTFUN1:def 2;
per cases ( x = li or x <> li ) ;
suppose A3: x = li ; :: thesis: (s +* (li,k)) . b1 in (the_Values_of SCMPDS) . b1
then A4: (the_Values_of SCMPDS) . x = Values li
.= INT by SCMPDS_2:5 ;
(s +* (li,k)) . x = k by A1, A3, FUNCT_7:31;
hence (s +* (li,k)) . x in (the_Values_of SCMPDS) . x by A4, INT_1:def 2; :: thesis: verum
end;
suppose x <> li ; :: thesis: (s +* (li,k)) . b1 in (the_Values_of SCMPDS) . b1
then (s +* (li,k)) . x = s . x by FUNCT_7:32;
hence (s +* (li,k)) . x in (the_Values_of SCMPDS) . x by A2, FUNCT_1:def 14; :: thesis: verum
end;
end;
end;
hence s +* (li,k) is PartState of SCMPDS by FUNCT_1:def 14; :: thesis: verum