let x be bound_QC-variable; :: thesis: for a being free_QC-variable holds a .--> x is Substitution
let a be free_QC-variable; :: thesis: a .--> x is Substitution
set f = a .--> x;
( a in free_QC-variables & x in QC-variables & dom (a .--> x) = {a} & rng (a .--> x) = {x} ) by FUNCOP_1:14, FUNCOP_1:19;
then ( dom (a .--> x) c= free_QC-variables & rng (a .--> x) c= QC-variables ) by ZFMISC_1:37;
hence a .--> x is Substitution by RELSET_1:11; :: thesis: verum