A1: IC in dom p by Def11;
dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
hence IC in dom (p +* d) by A1, XBOOLE_0:def 3; :: according to MEMSTR_0:def 11 :: thesis: IC (p +* d) = k
not IC in dom d by Th10;
hence IC (p +* d) = IC p by FUNCT_4:11
.= k by Def11 ;
:: thesis: verum