let x be object ; :: according to FUNCT_1:def 14 :: thesis: ( not x in dom (s +* (li,k)) or (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x )
assume x in dom (s +* (li,k)) ; :: thesis: (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x
then A1: x in dom s by FUNCT_7:30;

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

suppose A2: x = li ; :: thesis: (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x

then A3: (the_Values_of SCM+FSA) . x = Values li
.= INT by SCMFSA_2:11 ;
(s +* (li,k)) . x = k by A2, A1, FUNCT_7:31;
hence (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x by A3, INT_1:def 2; :: thesis: verum

end;

suppose x <> li ; :: thesis: (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x

then (s +* (li,k)) . x = s . x by FUNCT_7:32;
hence (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x by A1, FUNCT_1:def 14; :: thesis: verum

end;

end;