( dom (x .--> y) = {x} & rng (x .--> y) = {y} ) by FUNCOP_1:14, FUNCOP_1:19;
then x .--> y is PartFunc of bound_QC-variables ,bound_QC-variables by RELSET_1:11;
hence Sbst x,y is CQC_Substitution by PARTFUN1:119, SUBSTUT1:def 1; :: thesis: verum