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