let k be Element of NAT ; :: thesis: for l being CQC-variable_list of k
for i being Element of NAT st 1 <= i & i <= len l holds
l . i in bound_QC-variables
let l be CQC-variable_list of k; :: thesis: for i being Element of NAT st 1 <= i & i <= len l holds
l . i in bound_QC-variables
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len l implies l . i in bound_QC-variables )
A1: rng l c= bound_QC-variables by CQC_LANG:def 5;
assume ( 1 <= i & i <= len l ) ; :: thesis: l . i in bound_QC-variables
then i in dom l by FINSEQ_3:27;
then l . i in rng l by FUNCT_1:def 5;
hence l . i in bound_QC-variables by A1; :: thesis: verum