let Al be QC-alphabet ; :: thesis: for i, k being Nat
for ll being CQC-variable_list of k,Al st i in dom ll holds
ll . i is bound_QC-variable of Al
let i, k be Nat; :: thesis: for ll being CQC-variable_list of k,Al st i in dom ll holds
ll . i is bound_QC-variable of Al
let ll be CQC-variable_list of k,Al; :: thesis: ( i in dom ll implies ll . i is bound_QC-variable of Al )
assume i in dom ll ; :: thesis: ll . i is bound_QC-variable of Al
then A1: ll . i in rng ll by FUNCT_1:3;
rng ll c= bound_QC-variables Al by RELAT_1:def 19;
hence ll . i is bound_QC-variable of Al by A1; :: thesis: verum