v is Element of Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;
then ex f being Function st
( v = f & dom f = bound_QC-variables Al & rng f c= A ) by FUNCT_2:def 2;
then dom (v +* vS) = (bound_QC-variables Al) \/ (dom vS) by FUNCT_4:def 1;
then A1: dom (v +* vS) = bound_QC-variables Al by XBOOLE_1:12;
rng (v +* vS) c= (rng v) \/ (rng vS) by FUNCT_4:17;
then v +* vS in Funcs ((bound_QC-variables Al),A) by A1, FUNCT_2:def 2;
hence . is Element of Valuations_in (Al,A) by VALUAT_1:def 1; :: thesis: verum