let k be Element of NAT ; :: thesis: for f being CQC-variable_list of k holds f is FinSequence of bound_QC-variables
let f be CQC-variable_list of k; :: thesis: f is FinSequence of bound_QC-variables
rng f c= bound_QC-variables by CQC_LANG:def 5;
hence f is FinSequence of bound_QC-variables by FINSEQ_1:def 4; :: thesis: verum