let x be set ; :: according to FUNCT_1:def 14 :: thesis: ( not x in proj1 (s +* ((IC ),l)) or (s +* ((IC ),l)) . x in the Object-Kind of S . x )
assume x in dom (s +* ((IC ),l)) ; :: thesis: (s +* ((IC ),l)) . x in the Object-Kind of S . x
then A: x in dom s by FUNCT_7:30;

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

suppose S: x = IC ; :: thesis: (s +* ((IC ),l)) . x in the Object-Kind of S . x

then B: (s +* ((IC ),l)) . x = l by A, FUNCT_7:31;
ObjectKind (IC ) = NAT by Def6;
hence (s +* ((IC ),l)) . x in the Object-Kind of S . x by S, B; :: thesis: verum

end;

suppose x <> IC ; :: thesis: (s +* ((IC ),l)) . x in the Object-Kind of S . x

then (s +* ((IC ),l)) . x = s . x by FUNCT_7:32;
hence (s +* ((IC ),l)) . x in the Object-Kind of S . x by A, FUNCT_1:def 14; :: thesis: verum

end;

end;