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