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