A1: ( dom p = Bags n & dom q = Bags n ) by FUNCT_2:def 1;
dom (p + q) = (dom p) /\ (dom q) by VFUNCT_1:def 1;
hence p + q is Series of n,L by A1, FUNCT_2:130; :: thesis: verum