A: IC S in dom p by Def41;
dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
hence IC S in dom (p +* d) by A, XBOOLE_0:def 3; :: according to COMPOS_1:def 16 :: thesis: IC (p +* d) = k
not IC S in dom d by Th22;
hence IC (p +* d) = IC p by FUNCT_4:12
.= k by Def41 ;
:: thesis: verum