A1: IC in dom q by Def16;
dom q c= dom (p +* q) by FUNCT_4:11;
hence IC in dom (p +* q) by A1; :: according to COMPOS_1:def 16 :: thesis: IC (p +* q) = l
IC q = l by Def16;
hence IC (p +* q) = l by A1, FUNCT_4:14; :: thesis: verum