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