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