A1: IC in dom q by Def16;
dom q c= dom (p +* q) by FUNCT_4:10;
hence IC in dom (p +* q) by A1; :: according to MEMSTR_0:def 8 :: thesis: IC (p +* q) = l
IC q = l by Def16;
hence IC (p +* q) = l by A1, FUNCT_4:13; :: thesis: verum