A1: ( x .--> y is CQC_Substitution of Al iff x .--> y is Element of PFuncs ((bound_QC-variables Al),(bound_QC-variables Al)) ) by SUBSTUT1:def 1;
( dom (x .--> y) = {x} & rng (x .--> y) = {y} ) by FUNCOP_1:8;
then x .--> y is PartFunc of (bound_QC-variables Al),(bound_QC-variables Al) by RELSET_1:4;
hence Sbst (y,) is CQC_Substitution of Al by A1, PARTFUN1:45; :: thesis: verum