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

( 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