rng (v +* w) c= (rng v) \/ (rng w) by FUNCT_4:18;
then ( dom (v +* w) = (dom v) \/ (dom w) & rng (v +* w) c= A ) by FUNCT_4:def 1, XBOOLE_1:1;
hence w . is Val_Sub of A by RELSET_1:11; :: thesis: verum