let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for a being free_QC-variable of A holds a .--> x is Substitution of A
let x be bound_QC-variable of A; :: thesis: for a being free_QC-variable of A holds a .--> x is Substitution of A
let a be free_QC-variable of A; :: thesis: a .--> x is Substitution of A
set f = a .--> x;
rng (a .--> x) = {x} by FUNCOP_1:8;
then A1: rng (a .--> x) c= QC-variables A by ZFMISC_1:31;
dom (a .--> x) c= free_QC-variables A by ZFMISC_1:31;
hence a .--> x is Substitution of A by A1, RELSET_1:4; :: thesis: verum