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