thus IC in dom (DecIC (p,k)) by Th64; :: according to MEMSTR_0:def 11 :: thesis: IC (DecIC (p,k)) = 0
thus IC (DecIC (p,k)) = (IC p) -' k by Th65
.= k -' k by Def11
.= 0 by XREAL_1:232 ; :: thesis: verum