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;
rng (a .--> x) = {x} by FUNCOP_1:8;
then A1: rng (a .--> x) c= QC-variables by ZFMISC_1:31;
dom (a .--> x) = {a} by FUNCOP_1:13;
then dom (a .--> x) c= free_QC-variables by ZFMISC_1:31;
hence a .--> x is Substitution by A1, RELSET_1:4; :: thesis: verum