let x be object ; :: according to FUNCT_1:def 14 :: thesis: ( not x in dom (s +* ((IC ),l)) or (s +* ((IC ),l)) . x in (the_Values_of S) . x )
assume x in dom (s +* ((IC ),l)) ; :: thesis: (s +* ((IC ),l)) . x in (the_Values_of S) . x
then A1: x in dom s by FUNCT_7:30;
per cases ( x = IC or x <> IC ) ;
suppose A2: x = IC ; :: thesis: (s +* ((IC ),l)) . x in (the_Values_of S) . x
then A3: (s +* ((IC ),l)) . x = l by A1, FUNCT_7:31;
reconsider l = l as Element of NAT by ORDINAL1:def 12;
Values (IC ) = NAT by Def6;
then (s +* ((IC ),l)) . x in (the_Values_of S) . x by A2, A3;
hence (s +* ((IC ),l)) . x in (the_Values_of S) . x ; :: thesis: verum
end;
suppose x <> IC ; :: thesis: (s +* ((IC ),l)) . x in (the_Values_of S) . x
then (s +* ((IC ),l)) . x = s . x by FUNCT_7:32;
hence (s +* ((IC ),l)) . x in (the_Values_of S) . x by A1, FUNCT_1:def 14; :: thesis: verum
end;
end;