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